Sound Sequentialization for Concurrent Program Verification
summary
Transforms concurrent code into a sequential program via sound sequentialization that picks one representative per commutativity equivalence class using positional lexicographic preference orders, implements reductions with sleep set + weakly persistent sets, and integrates into a Trace Abstraction style verifier in the Ultimate toolchain (GEMCutter plugin). It proves safety properties including arbitrary asserts, scales better than naive interleavings (verifies ~50 more SV-COMP/Viva benchmarks, ~50% time, ~27% memory, ~64% fewer proof steps).
AI-written summary · about
chapters (4)
related talks
23mStratified Commutativity in Verification Algorithms for Concurrent Programs
21mCommCSL: Proving Information Flow Security for Concurrent Programs using Abstract(…)
15mSoundness of Predictive Concurrency Analyses
19mScenario-based Proofs for Concurrent Objects
24mSimuliris: A Separation Logic Framework for Verifying Concurrent Program Optimiz
30mMonadic interpreters for concurrent memory models: Executable semantics of a concurrent(…)
19mCompCertOC: Verified Compositional Compilation of Multi-threaded Programs with Shared(…)
32mCorrectness Witnesses for Concurrent Programs: Bridging the Semantic Divide with Ghosts