Detail aplikovaného výsledku

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.

Originální název

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

Anglický název

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

Druh

Software

Abstrakt

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.

Abstrakt aglicky

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.

Klíčová slova

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

Klíčová slova anglicky

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

Umístění

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

Licenční poplatek

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

www

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