A Primal-Dual Perspective on Program Verification Algorithms

Explore a groundbreaking 19-minute conference talk from POPL 2025 that introduces a unified primal-dual framework for program verification algorithms. Presented by researchers from Chiba University, Tohoku University, Weizmann Institute of Science, and Tel Aviv University, this talk demonstrates how concepts from optimization theory can be applied to verification problems. Learn how the researchers generalize the concept of a Lagrangian to capture discrete domains common in verification, enabling the simultaneous search for primal and dual solutions that guide each other. Discover how many existing algorithms in program analysis and verification can be derived from this framework, providing new insights into their characteristics. The presentation also introduces a novel validity checking algorithm for fixpoint logic over quantified linear arithmetic, with a prototype implementation showing promising results on instances that challenge state-of-the-art techniques. This theoretical advancement offers a fresh perspective on leveraging duality in program verification and automated reasoning.