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

software

anglicky

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

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

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

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

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, zahájení: 2020-01-01, ukončení: 2024-12-31, ukonč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á skupina automatizované analýzy a verifikace - VeriFIT (VZ VERIFIT)

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