License: 
Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.MFCS.2019.1
URN: urn:nbn:de:0030-drops-109456
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2019/10945/
Abdulaziz, Mohammad ;
Mehlhorn, Kurt ;
Nipkow, Tobias
Trustworthy Graph Algorithms (Invited Talk)
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.
BibTeX - Entry
@InProceedings{abdulaziz_et_al:LIPIcs:2019:10945,
author = {Mohammad Abdulaziz and Kurt Mehlhorn and Tobias Nipkow},
title = {{Trustworthy Graph Algorithms (Invited Talk)}},
booktitle = {44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)},
pages = {1:1--1:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-117-7},
ISSN = {1868-8969},
year = {2019},
volume = {138},
editor = {Peter Rossmanith and Pinar Heggernes and Joost-Pieter Katoen},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2019/10945},
URN = {urn:nbn:de:0030-drops-109456},
doi = {10.4230/LIPIcs.MFCS.2019.1},
annote = {Keywords: graph algorithms, formal correct proofs, Isabelle, LEDA, certifying algorithms}
}
|
Keywords: |
|
graph algorithms, formal correct proofs, Isabelle, LEDA, certifying algorithms |
|
Collection: |
|
44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019) |
|
Issue Date: |
|
2019 |
|
Date of publication: |
|
20.08.2019 |
