A Primal-Dual Perspective on Program Verification Algorithms
summary
Presents a unified algorithmic framework that generalizes Lagrangians to discrete domains (powersets, predicates, ranking functions) and runs an abstract primal-dual search that simultaneously builds candidate proofs and counterexamples. Proves progress under lattice monotonicity and shows CEGAR, ICE learning, primal‑dual Houdini, disjunctive rankings and strategy‑skeleton quantifier instantiation all instantiate the framework. Delivers a prototype validity checker for fixpoint logic over quantified linear arithmetic that outperforms some state‑of‑the‑art instances.
AI-written summary · about