Document Open Access Logo

Low-Level Bi-Abduction (Artifact)

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

PDF

Artifact Description

Thumbnail PDF
PDF
DARTS.8.2.11.pdf
  • Filesize: 0.58 MB
  • 6 pages

Document Identifiers

Subject Classification

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

Metrics

Artifact

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

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

Cite As Get 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) https://doi.org/10.4230/DARTS.8.2.11

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

Funding

The Czech authors were supported by the project 20-07487S of the Czech Science Foundation, the FIT BUT internal project FIT-S-20-6427, and L. Holík by the ERC.CZ project LL1908.

Related Article

  • Lukáš Holík, Petr Peringer, Adam Rogalewicz, Veronika Šoková, Tomáš Vojnar, and Florian Zuleger, "Low-Level Bi-Abduction", in 36th European Conference on Object-Oriented Programming (ECOOP 2022), LIPIcs, Vol. 222, pp. 19:1-19:30, 2022. https://doi.org/10.4230/LIPIcs.ECOOP.2022.19
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact