@inproceedings{a5be636a9043422cb4944e6fa8ae97c1,
title = "Trustworthy graph algorithms",
abstract = "The goal of the LEDA project was to build an easy-to-use and extendable library of correct and efficient data structures, graph algorithms and geometric algorithms. We report on the use of formal program verification to achieve an even higher level of trustworthiness. Specifically, we report on an ongoing and largely finished verification of the blossom-shrinking algorithm for maximum cardinality matching.",
keywords = "Certifying algorithms, Formal correct proofs, Graph algorithms, Isabelle, LEDA",
author = "Mohammad Abdulaziz and Kurt Mehlhorn and Tobias Nipkow",
note = "Publisher Copyright: {\textcopyright} Mohammad Abdulaziz, Kurt Mehlhorn, and Tobias Nipkow.; 44th International Symposium on Mathematical Foundations of Computer Science, MFCS 2019 ; Conference date: 26-08-2019 Through 30-08-2019",
year = "2019",
month = aug,
doi = "10.4230/LIPIcs.MFCS.2019.1",
language = "English",
series = "Leibniz International Proceedings in Informatics, LIPIcs",
publisher = "Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing",
editor = "Joost-Pieter Katoen and Pinar Heggernes and Peter Rossmanith",
booktitle = "44th International Symposium on Mathematical Foundations of Computer Science, MFCS 2019",
}