Correctness Witnesses for Concurrent Programs: Bridging the Semantic Divide with Ghosts
summary
Proposes a machine-readable ghost witness format that instruments programs with ghost variables and statements so a validator checks witness validity by analyzing the instrumented program; extends Witness 2.0 and targets both interleaving and thread-modular semantics, proving safety coincides across them. Implements witness generation in Goblin and validation in Ultimate Gem Cutter, evaluates on SV-COMP concurrency tasks, gets 75% confirmed, finds 29 bugs across tools, and observes modest runtime slowdowns for most validations.
AI-written summary · about
chapters (8)
- 0:00Introduction
- 15:00Witness validity semantics
- 17:11Local trace vs interleaving
- 17:57Ghost witness format
- 18:38Evaluation with Goblin & GemCutter
- 22:36Impact on tool quality
- 24:22Summary & future
- 25:09Q&A
related talks
21mThe Ghosts of Empires: Extracting Modularity from Interleaving-Based Proofs
24mA Concurrent Program Logic with a Future and History
31mVerified Software at Scale
01h 03mPrinciples of Persistent Programming
01h 00mCooperative Verification: Towards Reliable Safety-Critical Systems
30mTrustworthy Runtime Verification via Bisimulation
19mCompCertOC: Verified Compositional Compilation of Multi-threaded Programs with Shared(…)
01h 01mThe Future of Concurrency and Parallelism