Trustworthy Systems

Characteristic formulae for liveness properties of non-terminating CakeML programs


Johannes ├ůman Pohjola, Henrik Rostedt and Magnus Myreen


Chalmers University of Technology

UNSW Sydney


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

    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              = {},
    isbn             = {9783959771221},
    keywords         = {Program verification; non-termination; liveness; {Hoare} logic},
    month            = sep,
    pages            = {32:1-19},
    paperurl         = {},
    publisher        = {LIPIcs},
    title            = {Characteristic Formulae for Liveness Properties of Non-terminating {CakeML} Programs},
    volume           = {141},
    year             = {2019}