2026-07-26T02:32:23Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:16209 2024-03-06T11:05:15Z ddc:004 open_access

Low-Level Bi-Abduction (Artifact) Holík, Lukáš Peringer, Petr Rogalewicz, Adam Šoková, Veronika Vojnar, Tomáš Zuleger, Florian programs with dynamic linked data structures programs with pointers low-level pointer operations static analysis shape analysis separation logic bi-abduction 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Lukáš Holík and Petr Peringer and Adam Rogalewicz and Veronika Šoková and Tomáš Vojnar and Florian Zuleger 2022 Is Part Of DARTS, Volume 8, Issue 2, Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022) Article Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/DARTS.8.2.11 urn:nbn:de:0030-drops-162092 https://drops.dagstuhl.de/entities/document/10.4230/DARTS.8.2.11 eng https://creativecommons.org/licenses/by/4.0/legalcode