3 Search Results for "Madlener, Christoph"

Document
Short Paper
DOI: 10.4230/LIPIcs.ITP.2026.33
Formal Primal-Dual Algorithm Analysis (Short Paper)

Authors: Mohammad Abdulaziz, Thomas Ammer, and Christoph Madlener

Published in: LIPIcs, Volume 382, 17th International Conference on Interactive Theorem Proving (ITP 2026)

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

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)

Copy BibTex To Clipboard

@InProceedings{abdulaziz_et_al:LIPIcs.ITP.2026.33,
  author =	{Abdulaziz, Mohammad and Ammer, Thomas and Madlener, Christoph},
  title =	{{Formal Primal-Dual Algorithm Analysis}},
  booktitle =	{17th International Conference on Interactive Theorem Proving (ITP 2026)},
  pages =	{33:1--33:9},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-436-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{382},
  editor =	{Komendantskaya, Ekaterina and Nipkow, Tobias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.33},
  URN =		{urn:nbn:de:0030-drops-270075},
  doi =		{10.4230/LIPIcs.ITP.2026.33},
  annote =	{Keywords: Bipartite Matching, Graph Algorithms, Isabelle/HOL, Formal Verification}
}
Document
DOI: 10.4230/LIPIcs.ITP.2025.2
A Formal Analysis of Algorithms for Matroids and Greedoids

Authors: Mohammad Abdulaziz, Thomas Ammer, Shriya Meenakshisundaram, and Adem Rimpapa

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
We present a formal analysis, in Isabelle/HOL, of optimisation algorithms for matroids, which are useful generalisations of combinatorial structures that occur in optimisation, and greedoids, which are a generalisation of matroids. Although some formalisation work has been done earlier on matroids, our work here presents the first formalisation of results on greedoids, and many results we formalise in relation to matroids are also formalised for the first time in this work. We formalise the analysis of a number of optimisation algorithms for matroids and greedoids. We also derive from those algorithms executable implementations of Kruskal’s algorithm for computing optimal spanning trees, an algorithm for maximum cardinality matching for bi-partite graphs, and Prim’s algorithm for computing minimum weight spanning trees.
Cite as

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). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 2:1-2:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{abdulaziz_et_al:LIPIcs.ITP.2025.2,
  author =	{Abdulaziz, Mohammad and Ammer, Thomas and Meenakshisundaram, Shriya and Rimpapa, Adem},
  title =	{{A Formal Analysis of Algorithms for Matroids and Greedoids}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{2:1--2:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.2},
  URN =		{urn:nbn:de:0030-drops-246012},
  doi =		{10.4230/LIPIcs.ITP.2025.2},
  annote =	{Keywords: Matroids, Greedoids, Combinatorial Optimisation, Graph Algorithms, Isabelle/HOL, Formal Verification}
}
Document
DOI: 10.4230/LIPIcs.ITP.2023.3
A Formal Analysis of RANKING

Authors: Mohammad Abdulaziz and Christoph Madlener

Published in: LIPIcs, Volume 268, 14th International Conference on Interactive Theorem Proving (ITP 2023)

Abstract
We describe a formal correctness proof of RANKING, an online algorithm for online bipartite matching. An outcome of our formalisation is that it shows that there is a gap in all combinatorial proofs of the algorithm. Filling that gap constituted the majority of the effort which went into this work. This is despite the algorithm being one of the most studied algorithms and a central result in theoretical computer science. This gap is an example of difficulties in formalising graphical arguments which are ubiquitous in the theory of computing.
Cite as

Mohammad Abdulaziz and Christoph Madlener. A Formal Analysis of RANKING. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 3:1-3:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{abdulaziz_et_al:LIPIcs.ITP.2023.3,
  author =	{Abdulaziz, Mohammad and Madlener, Christoph},
  title =	{{A Formal Analysis of RANKING}},
  booktitle =	{14th International Conference on Interactive Theorem Proving (ITP 2023)},
  pages =	{3:1--3:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-284-6},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{268},
  editor =	{Naumowicz, Adam and Thiemann, Ren\'{e}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.3},
  URN =		{urn:nbn:de:0030-drops-183785},
  doi =		{10.4230/LIPIcs.ITP.2023.3},
  annote =	{Keywords: Matching Theory, Formalized Mathematics, Online Algorithms}
}
  • Refine by Type
  • 3 Document/PDF
  • 1 Document/HTML

  • Refine by Publication Year
  • 1 2026
  • 1 2025
  • 1 2023

  • Refine by Author
  • 3 Abdulaziz, Mohammad
  • 2 Ammer, Thomas
  • 2 Madlener, Christoph
  • 1 Meenakshisundaram, Shriya
  • 1 Rimpapa, Adem

  • Refine by Series/Journal
  • 3 LIPIcs

  • Refine by Classification
  • 2 Theory of computation → Discrete optimization
  • 2 Theory of computation → Invariants
  • 2 Theory of computation → Program verification
  • 1 Mathematics of computing
  • 1 Theory of computation

  • Refine by Keyword
  • 2 Formal Verification
  • 2 Graph Algorithms
  • 2 Isabelle/HOL
  • 1 Bipartite Matching
  • 1 Combinatorial Optimisation
  • Show More...

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