Document Open Access Logo

Refinement with Time - Refining the Run-Time of Algorithms in Isabelle/HOL

Authors Maximilian P. L. Haslbeck , Peter Lammich

PDF
Thumbnail PDF

File

LIPIcs.ITP.2019.20.pdf
  • Filesize: 0.49 MB
  • 18 pages

Document Identifiers

Author Details

Maximilian P. L. Haslbeck
  • Technische Universität München, Germany
Peter Lammich
  • The University of Manchester, England

Funding

  • Haslbeck, Maximilian P. L.: DFG Grant NI 491/16-1
  • Lammich, Peter: DFG Grant LA 3292/1 "Verifizierte Model Checker" and VeTSS grant "Formal Verification of Information Flow Security for Relational Databases"

Acknowledgements

We want to thank Simon Wimmer and Armaël Guéneau, as well as the anonymous reviewers for useful suggestions to improve the paper.

Cite As Get BibTex

Maximilian P. L. Haslbeck and Peter Lammich. Refinement with Time - Refining the Run-Time of Algorithms in Isabelle/HOL. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 20:1-20:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.ITP.2019.20

Abstract

Separation Logic with Time Credits is a well established method to formally verify the correctness and run-time of algorithms, which has been applied to various medium-sized use-cases. Refinement is a technique in program verification that makes software projects of larger scale manageable.
Combining these two techniques for the first time, we present a methodology for verifying the functional correctness and the run-time analysis of algorithms in a modular way. We use it to verify Kruskal’s minimum spanning tree algorithm and the Edmonds - Karp algorithm for network flow. 
An adaptation of the Isabelle Refinement Framework [Lammich and Tuerk, 2012] enables us to specify the functional result and the run-time behaviour of abstract algorithms which can be refined to more concrete algorithms. From these, executable imperative code can be synthesized by an extension of the Sepref tool [Lammich, 2015], preserving correctness and the run-time bounds of the abstract algorithm.

Subject Classification

ACM Subject Classification
  • Theory of computation → Program verification
  • Theory of computation → Separation logic
  • Theory of computation → Logic and verification
Keywords
  • Isabelle
  • Time Complexity Analysis
  • Separation Logic
  • Program Verification
  • Refinement
  • Run Time
  • Algorithms

Metrics

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

Supplementary Materials

References

  1. Robert Atkey. Amortised Resource Analysis with Separation Logic. In ESOP, volume 6012, pages 85-103. Springer, 2010. Google Scholar
  2. Lukas Bulwahn, Alexander Krauss, Florian Haftmann, Levent Erkok, and John Matthews. Imperative functional programming with Isabelle/HOL. Lecture Notes in Computer Science, 5170:134-149, 2008. Google Scholar
  3. Arthur Charguéraud. Characteristic Formulae for the Verification of Imperative Programs. In Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming, ICFP '11, pages 418-430, New York, NY, USA, 2011. ACM. URL: https://doi.org/10.1145/2034773.2034828.
  4. Arthur Charguéraud and François Pottier. Verifying the Correctness and Amortized Complexity of a Union-Find Implementation in Separation Logic with Time Credits. Journal of Automated Reasoning, pages 1-35, 2017. Google Scholar
  5. Javier Esparza, Peter Lammich, René Neumann, Tobias Nipkow, Alexander Schimpf, and Jan-Georg Smaus. A fully verified executable LTL model checker. In International Conference on Computer Aided Verification, pages 463-478. Springer, 2013. Google Scholar
  6. Mathias Fleury, Jasmin Christian Blanchette, and Peter Lammich. A verified SAT solver with watched literals using Imperative HOL. In Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, pages 158-171. ACM, 2018. Google Scholar
  7. Armaël Guéneau, Arthur Charguéraud, and François Pottier. A Fistful of Dollars: Formalizing Asymptotic Complexity Claims via Deductive Program Verification. In European Symposium on Programming (ESOP), 2018. Google Scholar
  8. Armaël Guéneau, Jacques-Henri Jourdan, Arthur Charguéraud, and François Pottier. Formal Proof and Analysis of an Incremental Cycle Detection Algorithm. In International Conference on Interactive Theorem Proving. Springer, 2019. URL: http://gallium.inria.fr/~agueneau/publis/gueneau-jourdan-chargueraud-pottier-2019.pdf.
  9. Maximilian P.L. Haslbeck, Peter Lammich, and Julian Biendarra. Kruskal’s Algorithm for Minimum Spanning Forest. Archive of Formal Proofs, February 2019. , Formal proof development. URL: http://isa-afp.org/entries/Kruskal.html.
  10. Peter Lammich. Verified efficient implementation of Gabow’s strongly connected component algorithm. In International Conference on Interactive Theorem Proving, pages 325-340. Springer, 2014. Google Scholar
  11. Peter Lammich. Refinement to Imperative/HOL. In International Conference on Interactive Theorem Proving, pages 253-269. Springer, 2015. Google Scholar
  12. Peter Lammich. Generating Verified LLVM from Isabelle/HOL. In International Conference on Interactive Theorem Proving. Springer, 2019. Google Scholar
  13. Peter Lammich and S Reza Sefidgar. Formalizing the edmonds-karp algorithm. In International Conference on Interactive Theorem Proving, pages 219-234. Springer, 2016. Google Scholar
  14. Peter Lammich and S. Reza Sefidgar. Formalizing the Edmonds-Karp Algorithm. Archive of Formal Proofs, August 2016. , Formal proof development. URL: http://isa-afp.org/entries/EdmondsKarp_Maxflow.html.
  15. Peter Lammich and Thomas Tuerk. Applying data refinement for monadic programs to Hopcroft’s algorithm. In International Conference on Interactive Theorem Proving, pages 166-182. Springer, 2012. Google Scholar
  16. Simon Wimmer and Peter Lammich. Verified model checking of timed automata. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 61-78. Springer, 2018. Google Scholar
  17. Bohua Zhan and Maximilian P. L. Haslbeck. Verifying asymptotic time complexity of imperative programs in Isabelle. In International Joint Conference on Automated Reasoning, pages 532-548. Springer, 2018. 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