Synthesizing History and Prophecy Variables for Symbolic Model Checking
Abstract elided by the publisher.
Related papers
- Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays TACAS 2021
- The future is ours: prophecy variables in separation logic POPL 2020
- Making prophecies with decision predicates POPL 2011
- Dynamic Programming for Symbolic Boolean Realizability and Synthesis CAV 2024
- Prophecy Made Simple TOPLAS 2022
- Model-checking concurrent systems with unbounded integer variables: symbolic representations, approximations, and experimental results TOPLAS 1999
- Thrust: A Prophecy-Based Refinement Type System for Rust PLDI 2025
- Multiple instances and symbolic variables in executable sequence charts OOPSLA 2002