Product detail

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

ROGALEWICZ, A. ŠOKOVÁ, V. VOJNAR, T. HOLÍK, L. PERINGER, P. ZULEGER, F.

Product type

software

Abstract

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.

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

Create date

5. 5. 2022

Location

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

Possibilities of use

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

Licence fee

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

www

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