Document Open Access Logo

Characteristic Formulae for Liveness Properties of Non-Terminating CakeML Programs

Authors Johannes Åman Pohjola, Henrik Rostedt, Magnus O. Myreen

PDF
Thumbnail PDF

File

LIPIcs.ITP.2019.32.pdf
  • Filesize: 0.51 MB
  • 19 pages

Document Identifiers

Author Details

Johannes Åman Pohjola
  • Data61/CSIRO, Sydney, Australia, University of New South Wales, Sydney, Australia
Henrik Rostedt
  • Chalmers University of Technology, Gothenburg, Sweden
Magnus O. Myreen
  • Chalmers University of Technology, Gothenburg, Sweden

Funding

  • Åman Pohjola, Johannes: This work was sponsored in part by the U.S. Defense Advanced Research Projects Agency (DARPA). The views expressed are those of the authors and do not reflect the official policy or position of the Defense Advanced Research Projects Agency (DARPA) or the U.S. Government. Approved for Public Release, Distribution Unlimited.
  • Myreen, Magnus O.: This work was supported by the Swedish Foundation for Strategic Research.

Acknowledgements

We are grateful to Robert Sison and the anonymous reviewers for many constructive and insightful comments.

Cite AsGet BibTex

Johannes Åman Pohjola, Henrik Rostedt, and Magnus O. Myreen. Characteristic Formulae for Liveness Properties of Non-Terminating CakeML Programs. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 32:1-32:19, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.ITP.2019.32

Abstract

There are useful programs that do not terminate, and yet standard Hoare logics are not able to prove liveness properties about non-terminating programs. This paper shows how a Hoare-like programming logic framework (characteristic formulae) can be extended to enable reasoning about the I/O behaviour of programs that do not terminate. The approach is inspired by transfinite induction rather than coinduction, and does not require non-terminating loops to be productive. This work has been developed in the HOL4 theorem prover and has been integrated into the ecosystem of proof tools surrounding the CakeML programming language.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Software verification
  • Theory of computation → Higher order logic
  • Theory of computation → Separation logic
Keywords
  • Program verification
  • non-termination
  • liveness
  • Hoare logic

Metrics

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

Supplementary Materials

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 Schloss Dagstuhl - LZI GmbH Imprint Privacy Contact