Formal Primal-Dual Algorithm Analysis
2026-04-22 • Logic in Computer Science
Logic in Computer ScienceDiscrete MathematicsData Structures and Algorithms
AI summaryⓘ
The authors describe their work on creating a formal framework and a library in Isabelle/HOL, a proof assistant, to rigorously verify algorithms that use primal-dual methods. They demonstrate this by formalizing several well-known matching algorithms, including the Hungarian Method, which is a classic primal-dual algorithm, and a modern algorithm used for assigning search queries to advertisers. Their effort helps ensure that these algorithms are mathematically correct and well understood.
Isabelle/HOLprimal-dual algorithmformal verificationmatching algorithmsHungarian MethodAdwords algorithmalgorithm analysisproof assistant
Authors
Mohammad Abdulaziz, Thomas Ammer
Abstract
We present an ongoing effort to build a framework and a library in Isabelle/HOL for formalising primal-dual arguments for the analysis of algorithms. We discuss a number of example formalisations from the theory of matching algorithms, covering classical algorithms like the Hungarian Method, widely considered the first primal-dual algorithm, and modern algorithms like the Adwords algorithm, which models the assignment of search queries to advertisers in the context of search engines.