License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ITP.2019.32
URN: urn:nbn:de:0030-drops-110872
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2019/11087/
Go to the corresponding LIPIcs Volume Portal

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

Characteristic Formulae for Liveness Properties of Non-Terminating CakeML Programs

pdf-format:
LIPIcs-ITP-2019-32.pdf (0.5 MB)

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.

BibTeX - Entry

@InProceedings{manpohjola_et_al:LIPIcs:2019:11087,
  author =	{Johannes Åman Pohjola and Henrik Rostedt and Magnus O. Myreen},
  title =	{{Characteristic Formulae for Liveness Properties of Non-Terminating CakeML Programs}},
  booktitle =	{10th International Conference on Interactive Theorem Proving (ITP 2019)},
  pages =	{32:1--32:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-122-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{141},
  editor =	{John Harrison and John O'Leary and Andrew Tolmach},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2019/11087},
  URN =		{urn:nbn:de:0030-drops-110872},
  doi =		{10.4230/LIPIcs.ITP.2019.32},
  annote =	{Keywords: Program verification, non-termination, liveness, Hoare logic}
}

Keywords: Program verification, non-termination, liveness, Hoare logic
Collection: 10th International Conference on Interactive Theorem Proving (ITP 2019)
Issue Date: 2019
Date of publication: 05.09.2019
Supplementary Material: This work has been developed in HOL4; the sources are at https://code.cakeml.org

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