Automating Relational Verification of Infinite-State Programs

Explore the challenges and approaches in automating relational verification of infinite-state programs in this conference talk from VMCAI'24. Delve into the complexities of verifying hyperproperties, including k-safety, generalized non-interference (GNI), and co-termination. Understand the importance of finding appropriate alignments for multiple execution traces and synthesizing relational invariants. Compare two key approaches: a constraint-based method extending Constrained Horn Clauses (CHCs) and a proof search technique within an inductive proof system for first-order fixpoint logic modulo theories. Gain insights into the significance of these verification techniques for program equivalence, non-interference, and security applications in infinite-state systems.