Product Details
Broom: A Static Analyzer for C Based on Separation Logic and the Principle of Bi-Abductive Reasoning
Created: 2022
Czech title
Broom: Nástroj pro statickou analýzu C programů založen na separační logice a bi-abdukčním přístupu
Type
software
License
In order to use the result by another entity, it is always necessary to acquire a license
License Fee
The licensor does not require a license fee for the result
Authors
Rogalewicz Adam, doc. Mgr., Ph.D.
(DITS)
Šoková Veronika, Ing. (DITS)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS)
Holík Lukáš, doc. Mgr., Ph.D. (DITS)
Peringer Petr, Dr. Ing. (DITS)
Zuleger Florian, Dr. (FIT)
Šoková Veronika, Ing. (DITS)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS)
Holík Lukáš, doc. Mgr., Ph.D. (DITS)
Peringer Petr, Dr. Ing. (DITS)
Zuleger Florian, Dr. (FIT)
Keywords
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
Description
Broom is a static analyzer for C written in OCaml. Broom primarily aims at programs that use low-level pointer manipulation to deal with various kinds of linked lists. It is based on separation logic and the principle of bi-abductive reasoning.
Location
License Conditions
Free software under the terms of GNU GPL (cf. http://www.gnu.org/licenses/gpl.html).
Projects
Efficient Finite Automata for Automated Reasoning, MŠMT, ERC CZ, LL1908, 2020-2024, running
Scalable Techniques for Analysis of Complex Properties of Computer Systems, GACR, Standardní projekty, GA20-07487S, 2020-2022, running
Spolehlivé, bezpečné a efektivní počítačové systémy, BUT, Vnitřní projekty VUT, FIT-S-20-6427, 2020-2023, completed
Scalable Techniques for Analysis of Complex Properties of Computer Systems, GACR, Standardní projekty, GA20-07487S, 2020-2022, running
Spolehlivé, bezpečné a efektivní počítačové systémy, BUT, Vnitřní projekty VUT, FIT-S-20-6427, 2020-2023, completed
Research groups
Departments