4 citations · 6 across the 4 of their papers we have counts for
5 papers · 1 filter
Deciding Boolean Separation Logic via Small Models (Technical Report)
Tomáš Dacík, Adam Rogalewicz, Tomáš Vojnar +1
We present a novel decision procedure for a fragment of separation logic (SL) with arbitrary nesting of separating conjunctions with boolean conjunctions, disjunctions, and guarded…
Compositional Shape Analysis with Shared Abduction and Biabductive Loop Acceleration (Extended Version)
Florian Sextl, Adam Rogalewicz, Tomáš Vojnar +1
Biabduction-based shape analysis is a compositional verification and analysis technique that can prove memory safety in the presence of complex, linked data structures. Despite its…
Low-Level Bi-Abduction
Lukáš Holík, Petr Peringer, Adam Rogalewicz +3
The paper proposes a new static analysis designed to handle open programs, i.e., fragments of programs, with dynamic pointer-linked data structures - in particular, various kinds o…
Fully Automated Shape Analysis Based on Forest Automata
Lukas Holik, Ondrej Lengal, Adam Rogalewicz +2
Forest automata (FA) have recently been proposed as a tool for shape analysis of complex heap structures. FA encode sets of tree decompositions of heap graphs in the form of tuples…
The Tree Width of Separation Logic with Recursive Definitions
Radu Iosif, Adam Rogalewicz, Jiri Simacek
Separation Logic is a widely used formalism for describing dynamically allocated linked data structures, such as lists, trees, etc. The decidability status of various fragments of…