DROPS

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.2024.3

A Formal Analysis of Capacity Scaling Algorithms for Minimum Cost Flows

Authors: Mohammad Abdulaziz and Thomas Ammer

Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)

Abstract

We present a formalisation of the correctness of algorithms to solve minimum-cost flow problems, in Isabelle/HOL. Two of the algorithms are based on the technique of scaling, most notably Orlin’s algorithm, which has the fastest running time for the problem of minimum-cost flow. Our work uncovered a number of complications in the proofs of the results we formalised, the resolution of which required significant effort. Our work is also the first to formally consider the problem of minimum-cost flows and, more generally, scaling algorithms.

Cite as

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

Copy BibTex To Clipboard

@InProceedings{abdulaziz_et_al:LIPIcs.ITP.2024.3,
  author =	{Abdulaziz, Mohammad and Ammer, Thomas},
  title =	{{A Formal Analysis of Capacity Scaling Algorithms for Minimum Cost Flows}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{3:1--3:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-337-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{309},
  editor =	{Bertot, Yves and Kutsia, Temur and Norrish, Michael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.3},
  URN =		{urn:nbn:de:0030-drops-207316},
  doi =		{10.4230/LIPIcs.ITP.2024.3},
  annote =	{Keywords: Network Flows, Formal Verification, Combinatorial Optimisation}
}

Search Results

Documents authored by Ammer, Thomas

A Formal Analysis of Algorithms for Matroids and Greedoids

Abstract

Cite as

A Formal Analysis of Capacity Scaling Algorithms for Minimum Cost Flows

Abstract

Cite as

Thanks for your feedback!

Could not send message