Document Open Access Logo

Formal Primal-Dual Algorithm Analysis (Short Paper)

Authors Mohammad Abdulaziz , Thomas Ammer , Christoph Madlener

PDF

File

Thumbnail PDF
PDF
LIPIcs.ITP.2026.33.pdf
  • Filesize: 0.73 MB
  • 9 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Discrete optimization
  • Theory of computation → Invariants
  • Theory of computation → Program verification
Keywords
  • Bipartite Matching
  • Graph Algorithms
  • Isabelle/HOL
  • Formal Verification

Metrics

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 As Get BibTex

Mohammad Abdulaziz, Thomas Ammer, and Christoph Madlener. Formal Primal-Dual Algorithm Analysis (Short Paper). In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 33:1-33:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.ITP.2026.33

Author Details

Mohammad Abdulaziz
  • King’s College London, UK
Thomas Ammer
  • King’s College London, UK
Christoph Madlener
  • Technische Universität München, Germany

Funding

  • Abdulaziz, Mohammad: Supported by the Renaissance Philanthropy Grant Co-Pilots for Isabelle and the Royal Society International Exchange grant Formal Verification of Practical Nominal Unification Algorithms (IES-R3-243187).
  • Ammer, Thomas: Supported by an ECR Travel Grant from the London Mathematical Society (LMS) to attend ITP.

Supplementary Materials

References

  1. Mohammad Abdulaziz. Graph Algorithms. In Functional Data Structures and Algorithms: A Proof Assistant Approach. Association for Computing Machinery, 2025. URL: https://doi.org/10.1145/3731369.3731394.
  2. Mohammad Abdulaziz and Thomas Ammer. A Formal Analysis of Capacity Scaling Algorithms for Minimum Cost Flows. In 15th International Conference on Interactive Theorem Proving (ITP), 2024. URL: https://doi.org/10.4230/LIPIcs.ITP.2024.3.
  3. Mohammad Abdulaziz and Thomas Ammer. A Formal Analysis of Capacity Scaling Algorithms for Minimum-Cost Flows, 2026. URL: https://doi.org/10.48550/arXiv.2602.03701.
  4. Mohammad Abdulaziz, Thomas Ammer, Ralitsa Dardjonova, Christoph Madlener, Shriya Meenakshisundaram, and Adem Rimpapa. Isabelle Graph Library. Accessed: May 24, 2026. URL: https://github.com/mabdula/isabelle-graph-library.
  5. Mohammad Abdulaziz, Thomas Ammer, Shriya Meenakshisundaram, and Adem Rimpapa. A Formal Analysis of Algorithms for Matroids and Greedoids. In 16th International Conference on Interactive Theorem Proving (ITP), 2025. URL: https://doi.org/10.4230/LIPIcs.ITP.2025.2.
  6. Mohammad Abdulaziz and Christoph Madlener. A Formal Analysis of RANKING. In The 14th Conference on Interactive Theorem Proving (ITP), 2023. URL: https://doi.org/10.4230/LIPIcs.ITP.2023.3.
  7. Mohammad Abdulaziz and Kurt Mehlhorn. A Formal Correctness Proof of Edmonds' Blossom Shrinking Algorithm. Journal of Automated Reasoning, 2026. URL: https://doi.org/10.1007/s10817-026-09747-y.
  8. Gagan Aggarwal, Gagan Goel, Chinmay Karande, and Aranyak Mehta. Online Vertex-Weighted Bipartite Matching and Single-bid Budgeted Allocations. In The 22nd Annual ACM-SIAM Symposium on Discrete Algorithms (SODA), 2011. URL: https://doi.org/10.1137/1.9781611973082.95.
  9. Clemens Ballarin. Interpretation of Locales in Isabelle: Theories and Proof Contexts. In Mathematical Knowledge Management, 2006. URL: https://doi.org/10.1007/11812289_4.
  10. Claude Berge. Two Theorems in Graph Theory. Proceedings of the National Academy of Sciences, 1957. URL: https://doi.org/10.1073/pnas.43.9.842.
  11. Benjamin E. Birnbaum and Claire Mathieu. On-Line Bipartite Matching Made Simple. SIGACT News, 2008. URL: https://doi.org/10.1145/1360443.1360462.
  12. Li Chen, Rasmus Kyng, Yang P. Liu, Richard Peng, Maximilian Probst Gutenberg, and Sushant Sachdeva. Maximum Flow and Minimum-Cost Flow in Almost-Linear Time. In 63rd IEEE Annual Symposium on Foundations of Computer Science (FOCS), 2022. URL: https://doi.org/10.1109/FOCS54457.2022.00064.
  13. Nikhil R. Devanur, Kamal Jain, and Robert D. Kleinberg. Randomized Primal-Dual Analysis of RANKING for Online Bipartite Matching. In The 24th Annual ACM-SIAM Symposium on Discrete Algorithms (SODA), 2013. URL: https://doi.org/10.1137/1.9781611973105.7.
  14. Manuel Eberl, Johannes Hölzl, and Tobias Nipkow. A Verified Compiler for Probability Density Functions. In Programming Languages and Systems - 24th European Symposium on Programming (ESOP), 2015. URL: https://doi.org/10.1007/978-3-662-46669-8_4.
  15. Alon Eden, Michal Feldman, Amos Fiat, and Kineret Segal. An Economics-Based Analysis of RANKING for Online Bipartite Matching. In Symposium on Simplicity in Algorithms (SOSA), 2021. URL: https://doi.org/10.1137/1.9781611976496.12.
  16. Jack Edmonds. Maximum Matching and a Polyhedron with 0,1-Vertices. Journal of Research of the National Bureau of Standards Section B Mathematics and Mathematical Physics, 1965. URL: https://doi.org/10.6028/jres.069B.013.
  17. Jack Edmonds. Paths, Trees, and Flowers. Canadian Journal of Mathematics, 1965. URL: https://doi.org/10.4153/CJM-1965-045-4.
  18. Robin Essmann, Tobias Nipkow, Simon Robillard, and Ujkan Sulejmani. Verified Approximation Algorithms. Logical Methods in Computer Science, 2022. URL: https://doi.org/10.46298/LMCS-18(1:36)2022.
  19. Gagan Goel and Aranyak Mehta. Online Budgeted Matching in Random Input Models with Applications to Adwords. In The 19th Annual ACM-SIAM Symposium on Discrete Algorithms (SODA), 2008. URL: https://doi.org/10.5555/1347082.1347189.
  20. Michel X. Goemans and David P. Williamson. The Primal-Dual Method for Approximation Algorithms and its Application to Network Design Problems. In Approximation Algorithms for NP-hard Problems. PWS, 1996. URL: https://math.mit.edu/~goemans/PAPERS/book-ch4.pdf.
  21. Zhiyi Huang, Ning Kang, Zhihao Gavin Tang, Xiaowei Wu, Yuhao Zhang, and Xue Zhu. Fully Online Matching. Journal of the ACM, 2020. URL: https://doi.org/10.1145/3390890.
  22. Zhiyi Huang, Zhihao Gavin Tang, Xiaowei Wu, and Yuhao Zhang. Fully Online Matching II: Beating Ranking and Water-filling. In 61st IEEE Annual Symposium on Foundations of Computer Science (FOCS), 2020. URL: https://doi.org/10.1109/FOCS46700.2020.00130.
  23. Carl Gustav Jacobi. De investigando Ordine Systematis Aequationum Differentialum vulgarium cuiuscumque. Journal für die reine und angewandte Mathematik, 1890. URL: https://www.lix.polytechnique.fr/~ollivier/JACOBI/Jacobi_De_Investigando.pdf.
  24. Bala Kalyanasundaram and Kirk Pruhs. An Optimal Deterministic Algorithm for Online B-Matching. Theoretical Computer Science, 2000. URL: https://doi.org/10.1016/S0304-3975(99)00140-1.
  25. Richard Manning Karp, Umesh Virkumar Vazirani, and Vijay V Vazirani. An Optimal Algorithm for On-Line Bipartite Matching. In The 22nd ACM Symposium on Theory of Computing (STOC), 1990. URL: https://doi.org/10.1145/100216.100262.
  26. Bernhard Korte and Jens Vygen. Combinatorial Optimization. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-24488-9.
  27. Harold W. Kuhn. The Hungarian Method for the Assignment Problem. Naval Research Logistics Quarterly, 1955. URL: https://doi.org/10.1002/nav.3800020109.
  28. Harold W. Kuhn. Variants of the Hungarian Method for Assignment Problems. Naval Research Logistics Quarterly, 1956. URL: https://doi.org/10.1002/nav.3800030404.
  29. Peter Lammich and Tobias Nipkow. Proof Pearl: Purely Functional, Simple and Efficient Priority Search Trees and Applications to Prim and Dijkstra. In 10th International Conference on Interactive Theorem Proving (ITP), 2019. URL: https://doi.org/10.4230/LIPIcs.ITP.2019.23.
  30. Peter Lammich and S. Reza Sefidgar. Formalizing Network Flow Algorithms: A Refinement Approach in Isabelle/HOL. Journal of Automated Reasoning, 2019. URL: https://doi.org/10.1007/s10817-017-9442-4.
  31. Aranyak Mehta, Amin Saberi, Umesh V. Vazirani, and Vijay V. Vazirani. AdWords and Generalized Online Matching. Journal of the ACM, 2007. URL: https://doi.org/10.1145/1284320.1284321.
  32. Milena Mihail and Thorben Tröbst. Online Matching with High Probability. In 17th International Symposium on Algorithmic Game Theory (SAGT), 2024. URL: https://doi.org/10.1007/978-3-031-71033-9_2.
  33. Julian Parsert. Linear Programming in Isabelle/HOL, 2024. URL: https://doi.org/10.48550/arXiv.2403.19639.
  34. Alexander Schrijver. Theory of Linear and Integer Programming. Wiley, 1986. Google Scholar
  35. Alexander Schrijver. Combinatorial Optimization: Polyhedra and Efficiency. Springer, 2003. Google Scholar
  36. Mirko Spasić and Filip Marić. Formalization of Incremental Simplex Algorithm by Stepwise Refinement. In FM 2012: Formal Methods, 2012. URL: https://doi.org/10.1007/978-3-642-32759-9_35.
  37. René Thiemann and Akihisa Yamada. Matrices, Jordan Normal Forms, and Spectral Radius Theory. Archive of Formal Proofs, 2015. , Formal Proof Development. URL: https://isa-afp.org/entries/Jordan_Normal_Form.html.
  38. Vijay V. Vazirani. Online Bipartite Matching and Adwords (Invited Talk). In The 47th International Symposium on Mathematical Foundations of Computer Science (MFCS), 2022. URL: https://doi.org/10.4230/LIPIcs.MFCS.2022.5.
  39. Vijay V. Vazirani. Towards a Practical, Budget-Oblivious Algorithm for the Adwords Problem under Small Bids. Algorithmica, 2026. URL: https://doi.org/10.1007/s00453-026-01369-5.
  40. Niklaus Wirth. Program Development by Stepwise Refinement. Communications of the ACM, 1971. URL: https://doi.org/10.1145/362575.362577.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact