Principles of Programming (PoP) Seminar - Oded Padon
August 27, 2026 3:30PM—4:30PM
Location:
In Person
-
Gates Hillman 8102
Speaker:
ODED PADON,
Senior Scientist, Faculty of Mathematics and Computer Science, Weizmann Institute of Science
https://www.wisdom.weizmann.ac.il/~padon/
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
—
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
Faculty Host: Bryan Parno
For More Information:
mstanle2@andrew.cmu.edu