Publication detail

Low-Level Bi-Abduction (Artifact)

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

Original Title

Low-Level Bi-Abduction (Artifact)

Type

miscellaneous

Language

English

Original 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.

Keywords

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

Authors

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

Released

23. 6. 2022

Location

Dagstuhl

Pages from

1

Pages to

6

Pages count

6

URL

http://dx.doi.org/10.4230/DARTS.8.2.11

BibTex

@misc{BUT178211,
  author="Adam {Rogalewicz} and Veronika {Šoková} and Tomáš {Vojnar} and Lukáš {Holík} and Petr {Peringer} and Florian {Zuleger}",
  title="Low-Level Bi-Abduction (Artifact)",
  year="2022",
  pages="1--6",
  address="Dagstuhl",
  doi="10.4230/DARTS.8.2.11",
  url="http://dx.doi.org/10.4230/DARTS.8.2.11",
  note="miscellaneous"
}