Broom: A Static Analyzer for C Based on Separation Logic and the Principle of Bi-Abductive Reasoning

Broom: Nástroj pro statickou analýzu C programů založen na separační logice a bi-abdukčním přístupu

software

In order to use the result by another entity, it is always necessary to acquire a license

The licensor does not require a license fee for the result

Rogalewicz Adam, doc. Mgr., Ph.D. (DITS)
Šoková Veronika, Ing. (DITS)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS)
Holík Lukáš, doc. Mgr., Ph.D. (DITS)
Peringer Petr, Dr. Ing. (DITS)
Zuleger Florian, Dr.

programs with dynamic linked data structures, programs with pointers, low-level
pointer operations, C, OCaml, static analysis, shape analyzer, separation logic,
bi-abduction, program verification

Broom is a static analyzer for C written in OCaml. Broom primarily aims at
programs that use low-level pointer manipulation to deal with various kinds of
linked lists. It is based on separation logic and the principle of bi-abductive
reasoning.

https://pajda.fit.vutbr.cz/rogalew/broom/-/tree/v0.0.1

Free software under the terms of GNU GPL (cf. http://www.gnu.org/licenses/gpl.html).

Efficient Finite Automata for Automated Reasoning, MŠMT, ERC CZ, LL1908, start: 2020-01-01, end: 2024-12-31, running
Scalable Techniques for Analysis of Complex Properties of Computer Systems, GACR, Standardní projekty, GA20-07487S, start: 2020-01-01, end: 2022-12-31, running
Spolehlivé, bezpečné a efektivní počítačové systémy, BUT, Vnitřní projekty VUT, FIT-S-20-6427, start: 2020-03-01, end: 2023-02-28, completed

Automated Analysis and Verification Research Group - VeriFIT (RG VERIFIT)

Department of Intelligent Systems (DITS)