Skip to main content

Characteristic formulae for liveness properties of non-terminating CakeML programs

Authors

Johannes ├ůman Pohjola, Henrik Rostedt and Magnus Myreen

DATA61

Chalmers University of Technology

UNSW Sydney

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 co-induction, 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{AAmanPohjola_RM_19,
    publisher        = {LIPIcs},
    doi              = {https://doi.org/10.4230/LIPIcs.ITP.2019.26},
    isbn             = {9783959771221},
    booktitle        = {Proceedings of the 10th International Conference on Interactive Theorem Proving},
    author           = {{\AA}man Pohjola, Johannes and Rostedt, Henrik and Myreen, Magnus},
    month            = sep,
    volume           = {141},
    keywords         = {Program verification; non-termination; liveness; {Hoare} logic},
    year             = {2019},
    date             = {2019-9-5},
    title            = {Characteristic Formulae for Liveness Properties of Non-terminating {CakeML} Programs},
    pages            = {32:1-19},
    address          = {Portland, Oregon}
  }

Download