3 papers
cs.SE2026
SEAL: Symbolic Execution with Separation Logic (Competition Contribution)
Tomáš Brablec, Tomáš Dacík, Tomáš Vojnar
SEAL is a static analyser for the verification of programs that manipulate unbounded linked data structures. It is based on separation logic to represent abstract memory states and…
cs.SE2025
RacerF: Data Race Detection with Frama-C (Competition Contribution)
Tomáš Dacík, Tomáš Vojnar
RacerF is a static analyser for detection of data races in multithreaded C programs implemented as a plugin of the Frama-C platform. The approach behind RacerF is mostly heuristic…
cs.LO2024
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…