Formal Primal-Dual Algorithm Analysis
Logic in Computer Science
2026-05-06 v2 Discrete Mathematics
Data Structures and Algorithms
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.
Cite
@article{arxiv.2604.20807,
title = {Formal Primal-Dual Algorithm Analysis},
author = {Mohammad Abdulaziz and Thomas Ammer and Christoph Madlener},
journal= {arXiv preprint arXiv:2604.20807},
year = {2026}
}