Low-Level Bi-Abduction (Artifact)

Authors Lukáš Holík , Petr Peringer , Adam Rogalewicz , Veronika Šoková , Tomáš Vojnar , Florian Zuleger

Thumbnail PDF

Artifact Description

  • Filesize: 0.58 MB
  • 6 pages

Document Identifiers

Author Details

Lukáš Holík
  • FIT, Brno University of Technology, Czech Republic
Petr Peringer
  • FIT, Brno University of Technology, Czech Republic
Adam Rogalewicz
  • FIT, Brno University of Technology, Czech Republic
Veronika Šoková
  • FIT, Brno University of Technology, Czech Republic
Tomáš Vojnar
  • FIT, Brno University of Technology, Czech Republic
Florian Zuleger
  • Faculty of Informatics, TU Wien, Austria

Cite AsGet BibTex

Lukáš Holík, Petr Peringer, Adam Rogalewicz, Veronika Šoková, Tomáš Vojnar, and Florian Zuleger. Low-Level Bi-Abduction (Artifact). In Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022). Dagstuhl Artifacts Series (DARTS), Volume 8, Issue 2, pp. 11:1-11:6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Artifact Evaluation Policy

The artifact has been evaluated as described in the ECOOP 2022 Call for Artifacts and the ACM Artifact Review and Badging Policy


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 structures - in particular, various kinds of lists - that 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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Separation logic
  • Theory of computation → Logic and verification
  • Software and its engineering → Formal software verification
  • programs with dynamic linked data structures
  • programs with pointers
  • low-level pointer operations
  • static analysis
  • shape analysis
  • separation logic
  • bi-abduction


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail