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

Název česky

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

Typ

software

Licence

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

Licenční poplatek

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

Autoři

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.

Klíčová slova

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ů

Popis

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.

Umístění

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

Licenční podmínky

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).

Projekty

Efektivní konečné automaty pro automatické usuzování, MŠMT, ERC CZ, LL1908, zahájení: 2020-01-01, ukončení: 2024-12-31, řešení
Spolehlivé, bezpečné a efektivní počítačové systémy, VUT, Vnitřní projekty VUT, FIT-S-20-6427, zahájení: 2020-03-01, ukončení: 2023-02-28, ukončen
Škálovatelné techniky pro analýzu komplexních vlastností počítačových systémů, GAČR, Standardní projekty, GA20-07487S, zahájení: 2020-01-01, ukončení: 2022-12-31, ukončen

Výzkumné skupiny

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

Pracoviště

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