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: Lightweight Static Data Race Detection for C Code
Tomáš DacÃk, Tomáš Vojnar
We present a novel static analysis for thread-modular data race detection. Our approach exploits static analysis of sequential program behaviour whose results are generalised for m…
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…