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

K využití výsledku jiným subjektem je vždy nutné nabytí licence

Poskytovatel licence na výsledek nepožaduje licenční poplatek

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

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í, MŠMT, ERC CZ, LL1908, 2020-2024, řešení
Spolehlivé, bezpečné a efektivní počítačové systémy, VUT, Vnitřní projekty VUT, FIT-S-20-6427, 2020-2023, ukončen
Škálovatelné techniky pro analýzu komplexních vlastností počítačových systémů, GAČR, Standardní projekty, GA20-07487S, 2020-2022, řešení

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

Ústav inteligentních systémů (UITS)