License
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.MFCS.2019.1
URN: urn:nbn:de:0030-drops-109456
URL: https://drops.dagstuhl.de/opus/volltexte/2019/10945/
Go to the corresponding LIPIcs Volume Portal


Abdulaziz, Mohammad ; Mehlhorn, Kurt ; Nipkow, Tobias

Trustworthy Graph Algorithms (Invited Talk)

pdf-format:
LIPIcs-MFCS-2019-1.pdf (0.6 MB)


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
Seminar: 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)
Issue Date: 2019
Date of publication: 23.08.2019


DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI