Trustworthy Systems

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

Download