Correctness Witnesses for Concurrent Programs: Bridging the Semantic Divide with Ghosts
No abstract available.
Related papers
- GPS: navigating weak memory with ghosts, protocols, and separation OOPSLA 2014
- Bridging the gap between programming languages and hardware weak memory models POPL 2019
- The Ghosts of Empires: Extracting Modularity from Interleaving-Based Proofs POPL 2026
- Goblint Validator: Correctness Witness Validation by Abstract Interpretation - (Competition Contribution) TACAS 2024
- Bridging the Gap between Real-World and Formal Binary Lifting through Filtered-Simulation OOPSLA 2025
- Caper - Automatic Verification for Fine-Grained Concurrency ESOP 2017
- Verus: Verifying Rust Programs using Linear Ghost Types OOPSLA 2023
- Higher-order ghost state ICFP 2016