Products of Recursive Programs for Hypersafety Verification
summary
Proposes an algorithmic construction of an infinite family of product programs that reduce hypersafety of recursive programs to ordinary safety, using visibly pushdown languages to preserve call/return structure and concurrency-style schedulers (contextual orders) to pick reductions. Introduces composable canonical reductions as building blocks and a tool Hyrack that encodes products as VPA/grammar and SMT checks. Evaluation on 103 benchmarks (45% from prior work) outperforms sequential baselines, the automata encoding solves harder cases but is slower, five benchmarks remain unsolved.
AI-written summary · about
chapters (10)
- 0:00Recursive program products intro
- 1:26Existing product constructions limits
- 2:52Interleaving in recursive programs
- 4:17Soundness for product programs
- 6:46Reductions like recursive programs
- 8:30Well-nested shuffle for hypersafety
- 9:56Canonical reductions building blocks
- 11:41Implementation and experiments
- 12:45Research lessons learned
- 14:10Q&A
related talks
23mProductivity Verification for Functional Programs by Reduction to Termination Ve...
20mDeciding Asynchronous Hyperproperties for Recursive Programs
59mTowards static analyses and abstract domains for hyperproperties
25mRecursive Program Synthesis using Paramorphisms
15mClosing Remarks
19mSimplifying Safety Proofs with Forward-Backward Reasoning and Prophecy
18mDeferring the Details and Deriving Programs
30mRelatively Complete Verification of Probabilistic Programs