4 citations · 7 across the 8 of their papers we have counts for
9 papers
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…
Reasoning about Regular Properties: A Comparative Study
Tomáš Fiedor, Lukáš Holík, Martin Hruška +3
Several new algorithms for deciding emptiness of Boolean combinations of regular languages and of languages of alternating automata (AFA) have been proposed recently, especially in…
Perun: Performance Version System
Tomáš Fiedor, Jiří Pavela, Adam Rogalewicz +1
In this paper, we present Perun: an open-source tool suite for profiling-based performance analysis. At its core, Perun maintains links between project versions and the correspondi…
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…
Abstraction Refinement for Trace Inclusion of Infinite State Systems
Radu Iosif, Adam Rogalewicz, Tomas Vojnar
A \emph{data automaton} is a finite automaton equipped with variables (counters or registers) ranging over infinite data domains. A trace of a data automaton is an alternating sequ…
Deciding Entailments in Inductive Separation Logic with Tree Automata
Radu Iosif, Adam Rogalewicz, Tomas Vojnar
Separation Logic (SL) with inductive definitions is a natural formalism for specifying complex recursive data structures, used in compositional verification of programs manipulatin…
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…