Context-Bounded Verification of Context-Free Specifications
summary
Shows that context-bounded refinement where the implementation is a multistack pushdown automaton and the specification is a Dyck or input‑deterministic multistack pushdown language is decidable and coNP-complete. Proof reduces search for counterexamples to existential Presburger satisfiability using Parikh-image encodings, compressed‑word offsets, and a new analysis of interleavings via two‑dimensional VAS and an offset‑uniform VAS class. Special cases cover reference counting and re‑entrant locking; hardness already holds for deterministic regular specs.
AI-written summary · about
chapters (11)
- 0:00Context-bounded verification intro
- 1:14Refinement with context-free specs
- 4:02Multi-threaded refinement
- 5:51Multi-pushdown automata
- 7:35Dick language decidability
- 9:41Reference counting example
- 14:39NP refinement algorithm
- 18:16Trace decomposition
- 20:24Mismatch violations
- 23:18Complexity and future work
- 24:01Q&A