Document Open Access Logo

Trustworthy Graph Algorithms (Invited Talk)

Authors Mohammad Abdulaziz, Kurt Mehlhorn, Tobias Nipkow

PDF
Thumbnail PDF

File

LIPIcs.MFCS.2019.1.pdf
  • Filesize: 0.57 MB
  • 22 pages

Document Identifiers

Author Details

Mohammad Abdulaziz
  • TU München, Germany
Kurt Mehlhorn
  • MPI for Informatics, Saarbrücken, Germany
Tobias Nipkow
  • TU München, Germany

Cite As Get BibTex

Mohammad Abdulaziz, Kurt Mehlhorn, and Tobias Nipkow. Trustworthy Graph Algorithms (Invited Talk). In 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 138, pp. 1:1-1:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.MFCS.2019.1

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Design and analysis of algorithms
  • Software and its engineering → Formal software verification
  • Software and its engineering → Software libraries and repositories
Keywords
  • graph algorithms
  • formal correct proofs
  • Isabelle
  • LEDA
  • certifying algorithms

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Mohammad Abdulaziz, Kurt Mehlhorn, and Tobias Nipkow. A Correctness Proof of Edmonds' Blossom Shrinking Algorithm for Maximum Matchings in Graphs. forthcoming. Google Scholar
  2. Mohammad Abdulaziz, Michael Norrish, and Charles Gretton. Formally Verified Algorithms for Upper-Bounding State Space Diameters. J. Autom. Reasoning, 61(1-4):485-520, 2018. URL: https://doi.org/10.1007/s10817-018-9450-z.
  3. Mohammad Abdulaziz and Lawrence C. Paulson. An Isabelle/HOL Formalisation of Green’s Theorem. Archive of Formal Proofs, 2018, 2018. URL: https://www.isa-afp.org/entries/Green.html.
  4. Wolfgang Ahrendt, Bernhard Beckert, Richard Bubel, Reiner Hähnle, Peter H. Schmitt, and Mattias Ulbrich, editors. Deductive Software Verification - The KeY Book - From Theory to Practice, volume 10001 of Lecture Notes in Computer Science. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-49812-6.
  5. E. Alkassar, S. Böhme, K. Mehlhorn, and Ch. Rizkallah. A Framework for the Verification of Certifying Computations. Journal of Automated Reasoning (JAR), 52(3):241-273, 2014. A preliminary version appeared under the title "Verification of Certifying Computations" in CAV 2011, LCNS Vol 6806, pages 67 - 82. URL: http://arxiv.org/abs/1301.7462.
  6. E. Althaus and K. Mehlhorn. Maximum Network Flow with Floating Point Arithmetic. . Info. Proc. Lett., 66:109-113, 1998. URL: http://www.mpi-sb.mpg.de/~mehlhorn/ftp/Althaus-Mehlhorn-maxflow.ps.
  7. Lukas Bulwahn, Alexander Krauss, Florian Haftmann, Levent Erkök, and John Matthews. Imperative Functional Programming with Isabelle/HOL. In Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, pages 134-149, 2008. URL: https://doi.org/10.1007/978-3-540-71067-7_14.
  8. Arthur Charguéraud. Characteristic formulae for the verification of imperative programs. In Proceeding of the 16th ACM SIGPLAN international conference on Functional Programming, ICFP 2011, Tokyo, Japan, September 19-21, 2011, pages 418-430, 2011. URL: https://doi.org/10.1145/2034773.2034828.
  9. Ernie Cohen, Markus Dahlweid, Mark Hillebrand, Dirk Leinenbach, Michał Moskal, Thomas Santen, Wolfram Schulte, and Stephan Tobies. VCC: A practical system for verifying concurrent C. In Theorem Proving in Higher Order Logics (TPHOLs 2009), volume 5674 of LNCS, pages 23-42. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-03359-9_2.
  10. Sander R Dahmen, Johannes Hölzl, and Robert Y Lewis. Formalizing the Solution to the Cap Set Problem. arXiv, 2019. URL: http://arxiv.org/abs/1907.01449.
  11. Jose Divasón, Sebastiaan J. C. Joosten, René Thiemann, and Akihisa Yamada. A Verified Implementation of the Berlekamp-Zassenhaus Factorization Algorithm. J. Autom. Reasoning, 2019. published online. Google Scholar
  12. J. Edmonds. Maximum Matching and a polyhedron with 0,1 - vertices. Journal of Research of the National Bureau of Standards, 69B:125-130, 1965. Google Scholar
  13. Javier Esparza, Peter Lammich, René Neumann, Tobias Nipkow, Alexander Schimpf, and Jan-Georg Smaus. A Fully Verified Executable LTL Model Checker. In Computer Aided Verification - 25th International Conference, CAV 2013, pages 463-478, 2013. URL: https://doi.org/10.1007/978-3-642-39799-8_31.
  14. S. Fortune. Robustness Issues in Geometric Algorithms. In Proceedings of the 1st Workshop on Applied Computational Geometry: Towards Geometric Engineering (WACG'96), volume 1148 of LNCS Series, pages 9-13, 1996. Google Scholar
  15. H. N. Gabow. An efficient implementation of Edmonds' algorithm for maximum matching on graphs. J. ACM, 23:221-234, 1976. Google Scholar
  16. David Greenaway, June Andronick, and Gerwin Klein. Bridging the Gap: Automatic Verified Abstraction of C. In Interactive Theorem Proving, volume 7406 of LNCS, pages 99-115, 2012. Google Scholar
  17. Florian Haftmann, Alexander Krauss, Ondvej Kunvar, and Tobias Nipkow. Data Refinement in Isabelle/HOL. In S. Blazy, C. Paulin-Mohring, and D. Pichardie, editors, Interactive Theorem Proving (ITP 2013), volume 7998 of LNCS Series, pages 100-115, 2013. Google Scholar
  18. Florian Haftmann and Tobias Nipkow. Code Generation via Higher-Order Rewrite Systems. In M. Blume, N. Kobayashi, and G. Vidal, editors, Functional and Logic Programming (FLOPS 2010), volume 6009 of LNCS, pages 103-117. Springer, 2010. Google Scholar
  19. Lars Hupel and Tobias Nipkow. A Verified Compiler from Isabelle/HOL to CakeML. In A. Ahmed, editor, European Symposium on Programming (ESOP 2018), volume 10801 of LNCS, pages 999-1026. Springer, 2018. Google Scholar
  20. L. Kettner, K. Mehlhorn, S. Pion, S. Schirra, and C. Yap. Classroom Examples of Robustness Problems in Geometric Computations. . Computational Geometry: Theory and Applications (CGTA), 40:61-78, 2008. a preliminary version appeared in ESA 2004, LNCS 3221, pages 702 - 713. URL: http://www.mpi-sb.mpg.de/~mehlhorn/ftp/ClassRoomExample.ps.
  21. Gerwin Klein, June Andronick, Kevin Elphinstone, Gernot Heiser, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. seL4: Formal verification of an operating-system kernel. CACM, 53(6):107-115, 2010. Google Scholar
  22. B. Korte and J.Vygen. Combinatorial Optimization: Theory and Algorithms. Springer, 2012. Google Scholar
  23. Ramana Kumar, Magnus O. Myreen, Michael Norrish, and Scott Owens. CakeML: a verified implementation of ML. In The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, pages 179-192. ACM, 2014. Google Scholar
  24. Peter Lammich. Automatic Data Refinement. In Interactive Theorem Proving - 4th International Conference, ITP 2013, pages 84-99, 2013. URL: https://doi.org/10.1007/978-3-642-39634-2_9.
  25. Peter Lammich. Refinement to Imperative HOL. J. Autom. Reasoning, 62(4):481-503, 2019. URL: https://doi.org/10.1007/s10817-017-9437-1.
  26. Peter Lammich and S. Reza Sefidgar. Formalizing Network Flow Algorithms: A Refinement Approach in Isabelle/HOL. J. Autom. Reasoning, 62(2):261-280, 2019. URL: https://doi.org/10.1007/s10817-017-9442-4.
  27. LEDA (Library of Efficient Data Types and Algorithms). www.algorithmic-solutions.com. Google Scholar
  28. LEMON graph library. COIN-OR project. Google Scholar
  29. Xavier Leroy. A Formally Verified Compiler Back-end. Journal of Automated Reasoning, 43:363-446, 2009. Google Scholar
  30. R.M. McConnell, K. Mehlhorn, S. Näher, and P. Schweitzer. Certifying algorithms. Computer Science Review, 5(2):119-161, 2011. Google Scholar
  31. K. Mehlhorn and S. Näher. LEDA: A library of efficient data types and algorithms. In MFCS'89, volume 379 of LNCS Series, pages 88-106, 1989. Google Scholar
  32. K. Mehlhorn and S. Näher. The implementation of geometric algorithms. . In Proceedings of the 13th IFIP World Computer Congress, volume 1, pages 223-231. Elsevier Science B.V. North-Holland, Amsterdam, 1994. URL: http://www.mpi-sb.mpg.de/~mehlhorn/ftp/ifip94.ps.
  33. K. Mehlhorn and S. Näher. From Algorithms to Working Programs: On the Use of Program Checking in LEDA. In MFCS'98, volume 1450 of LNCS Series, pages 84-93, 1998. Google Scholar
  34. K. Mehlhorn and S. Näher. The LEDA Platform for Combinatorial and Geometric Computing. Cambridge University Press, 1999. Google Scholar
  35. Robin Milner. Logic for computable functions: description of a machine implementation. Technical report, Stanford University, 1972. Google Scholar
  36. Magnus O. Myreen and Scott Owens. Proof-producing translation of higher-order logic into pure and stateful ML. J. Funct. Program., 24(2-3):284-315, 2014. URL: https://doi.org/10.1017/S0956796813000282.
  37. Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS Series. Springer, 2002. Google Scholar
  38. Lars Noschinski. A Graph Library for Isabelle. Mathematics in Computer Science, 9:22-39, 2015. Google Scholar
  39. Lars Noschinski, Christine Rizkallah, and Kurt Mehlhorn. Verification of Certifying Computations through AutoCorres and Simpl. In NASA Formal Methods, volume 8430 of Lecture Notes in Computer Science, pages 46-61. Springer, 2014. Google Scholar
  40. Lawrence C Paulson. Isabelle: A generic theorem prover, volume 828. Springer, 1994. Google Scholar
  41. Norbert Schirmer. Verification of Sequential Imperative Programs in Isabelle/HOL. PhD thesis, Technische Universität München, 2006. Google Scholar
  42. Verisoft. http://www.verisoft.de/, 2007.
  43. Andrew Lumsdaine von Jeremy G. Siek, Lie-Quan Lee. The Boost Graph Library: User Guide and Reference Manual. Addison-Wesley Professional, 2001. Google Scholar
  44. C.-K. Yap. Towards Exact Geometric Computation. CGTA: Computational Geometry: Theory and Applications, 7, 1997. Google Scholar
  45. C.-K. Yap. Robust geometric computation. In J.E. Goodman and J. O'Rourke, editors, Handbook of Discrete and Computational Geometry, chapter 41. CRC Press LLC, Boca Raton, FL, 2nd edition, 2003. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact