Publication Details

Low-Level Bi-Abduction (Artifact)

HOLÍK Lukáš, PERINGER Petr, ROGALEWICZ Adam, ŠOKOVÁ Veronika, VOJNAR Tomáš and ZULEGER Florian. Low-Level Bi-Abduction (Artifact). Dagstuhl, 2022. Available from: http://dx.doi.org/10.4230/DARTS.8.2.11
Czech title
Nízkoúrovňová Bi-abdukce (Artefakt)
Type
miscellaneous
Language
english
Authors
Holík Lukáš, doc. Mgr., Ph.D. (DITS FIT BUT)
Peringer Petr, Dr. Ing. (DITS FIT BUT)
Rogalewicz Adam, doc. Mgr., Ph.D. (DITS FIT BUT)
Šoková Veronika, Ing. (DITS FIT BUT)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS FIT BUT)
Zuleger Florian, Dr. (FORSYTE)
URL
Keywords

programs with dynamic linked data structures, programs with pointers, low-level pointer operations, static analysis, shape analysis, separation logic, bi-abduction

Abstract

Broom is a new static analyzer for C written in OCaml. Broom primarily aims at open programs, i.e., fragments of programs, with dynamic pointer-linked data structuresin particular, various kinds of liststhat employ advanced low-level pointer operations. It is based on separation logic and the
principle of bi-abductive reasoning. The artifact is a VirtualBox image of a Linux machine with Ubuntu 20.04 operating system. It contains source code and binary of the Broom tool, benchmarks, and scripts for running our and the competing tools we compare to.

Published
2022
Pages
1-6
Place
Dagstuhl, DE
DOI
10.4230/DARTS.8.2.11
BibTeX 
@MISC{FITPUB12747,
   author = "Luk\'{a}\v{s} Hol\'{i}k and Petr Peringer and Adam Rogalewicz and Veronika \v{S}okov\'{a} and Tom\'{a}\v{s} Vojnar and Florian Zuleger",
   title = "Low-Level Bi-Abduction (Artifact)",
   pages = "1--6",
   year = 2022,
   location = "Dagstuhl, DE",
   doi = "10.4230/DARTS.8.2.11",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/12747"
}
Back to top