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

vyžadována - zdarma

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

programy s dynamickými pointerovými datovými strukturami, programy s ukazateli, nízkoúrovňové operace, C, OCaml, statický analyzátor, analýza tvaru, separační logika, bi-abdukce, verifikace programů

Broom je statický analyzátor programů v C napsán v OCamli. Nástroj Broom přináší novou techniku statické analýzy určené pro otevřené programy (fragmenty programů) s dynamickými pointerovými datovými strukturami, konkrétně různými typy linkových listů. Technika je založena na separační logice a bi-abdukčním přístupu.

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

Volně šiřitelný software poskytovaný pod licencí GNU GPL (přesné znění licence je dostupné na stránce http://www.gnu.org/licenses/gpl.html).

Efektivní konečné automaty pro automatické usuzování (LL1908)
Spolehlivé, bezpečné a efektivní počítačové systémy (FIT-S-20-6427)
Škálovatelné techniky pro analýzu komplexních vlastností počítačových systémů (GA20-07487S)

Výzkumná skupina automatizované analýzy a verifikace - VeriFIT (VZ VERIFIT)

Ústav inteligentních systémů FIT VUT v Brně (UITS FIT VUT)