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

required - free

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

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 (LL1908)
Reliable, Secure, and Efficient Computer Systems (FIT-S-20-6427)
Scalable Techniques for Analysis of Complex Properties of Computer Systems (GA20-07487S)

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

Department of Intelligent Systems FIT BUT (DITS FIT BUT)