DARTS.8.2.11.pdf
- Filesize: 0.58 MB
- 6 pages
Document
Low-Level Bi-Abduction (Artifact)
Authors
Lukáš Holík 
,
Petr Peringer ,
Adam Rogalewicz ,
Veronika Šoková ,
Tomáš Vojnar ,
Florian Zuleger
-
Part of:
Issue:
Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022)
Volume: DARTS, Volume 8 (ECOOP 2022)
Conference: European Conference on Object-Oriented Programming (ECOOP)
Journal: Dagstuhl Artifacts Series (DARTS) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2022-06-23
Artifact Description
Document Identifiers
Author Details
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)
https://doi.org/10.4230/DARTS.8.2.11
https://doi.org/10.4230/DARTS.8.2.11
Artifact
DARTS-8-2-11-artifact-101f2587490f8f755abecd453e2c01d1.zip
(Filesize: 4.89 GB)
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.
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
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads