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

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 AsGet 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
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