Result Details

Low-Level Bi-Abduction (Artifact)

ROGALEWICZ, A.; ŠOKOVÁ, V.; VOJNAR, T.; HOLÍK, L.; PERINGER, P.; ZULEGER, F. Low-Level Bi-Abduction (Artifact). Dagstuhl: 2022. p. 1-6.
Type
other unclassified results
Language
English
Authors
Rogalewicz Adam, doc. Mgr., Ph.D., DITS (FIT)
Šoková Veronika, Ing., Ph.D.
Vojnar Tomáš, prof. Ing., Ph.D., DITS (FIT)
Holík Lukáš, doc. Mgr., Ph.D., DITS (FIT)
Peringer Petr, Dr. Ing., DITS (FIT)
Zuleger Florian, Dr., FIT (FIT)
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

URL
Published
2022
Pages
1–6
Place
Dagstuhl
DOI
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="Other unclassified results"
}
Projects
Efficient Finite Automata for Automated Reasoning, MŠMT, ERC CZ, LL1908, start: 2020-01-01, end: 2024-12-31, completed
Scalable Techniques for Analysis of Complex Properties of Computer Systems, GACR, Standardní projekty, GA20-07487S, start: 2020-01-01, end: 2022-12-31, completed
Spolehlivé, bezpečné a efektivní počítačové systémy, BUT, Vnitřní projekty VUT, FIT-S-20-6427, start: 2020-03-01, end: 2023-02-28, completed
Research groups
Automated Analysis and Verification Research Group - VeriFIT (RG VERIFIT)
Departments
Department of Intelligent Systems (DITS)
Back to top