Detail produktu

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

Vznik: 2022

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
vyžadována - zdarma
Autoři
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)
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í
Licence

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
Výzkumné skupiny
Pracoviště
Nahoru