PoP Seminar Talk

Duality and Primal-Dual Algorithms in Verification

Oded Padon, Senior Scientist in the Faculty of Mathematics and Computer Science at the Weizmann Institute of Science
Thursday, 27 August, 2026; 3:30pm
GHC 8102
Host: Bryan Parno

Abstract

Many algorithms and techniques in verification, program analysis, program synthesis, and automated reasoning 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 unifying framework for expressing verification algorithms as primal-dual algorithms. The framework generalizes the concept of a Lagrangian that is commonly used in linear 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