Duality and Primal-Dual Algorithms in Verification
5/12/2025, 3:00pm
Speaker
Abstract
Many of the algorithms and techniques developed in verification, program analysis, and program synthesis have a primal-dual flavor, which is usually informal. For example, an algorithm might simultaneously search for a proof and a counterexample, where the two searches guide each other. In this talk I will explore this perspective and discuss two technical contributions. The first is a new algorithm for invariant inference, i.e., automatically finding inductive invariants, that is based on a new formal duality between execution traces and a certain type of induction proofs. Unlike most verification algorithms, this algorithm is based on a formal duality, which is surprisingly symmetric. The second contribution is a unified framework for expressing verification algorithms as primal-dual algorithms. The framework generalizes the concept of a Lagrangian that is commonly used in linear programming and optimization in a way that captures many existing algorithms in verification and formally reveals their primal-dual nature.
Bio
Oded Padon is a senior scientist in the Faculty of Mathematics and Computer Science at the Weizmann Institute of Science. Oded joined Weizmann in September 2024, and prior to that he was a senior researcher at VMware Research, a postdoc in Alex Aiken's group at Stanford University, and a PhD student at Tel Aviv University advised by Mooly Sagiv. Oded's research interests include programming languages, formal verification, and distributed systems.