Trustworthy Systems

Verified characteristic formulae for CakeML

Authors

Armaël Guéneau, Magnus Myreen, Ramana Kumar and Michael Norrish

Ecole Normale Supérieure de Lyon

Chalmers University of Technology

Data61
CSIRO

UNSW

Australian National University

Abstract

Characteristic Formulae (CF) offer a productive, principled approach to generating verification conditions for higher-order imperative programs, but so far the soundness of CF has only been considered for informally specified programming languages (OCaml). This leaves a gap between what is established by the verification framework and the program that actually runs. We present a fully-fledged CF framework for the formally specified CakeML programming language. Our framework extends the existing CF approach to support exceptions and I/O, thereby covering the full feature set of CakeML, and comes with a formally verified soundness theorem. Furthermore, it integrates with existing proof techniques for verifying CakeML programs. This validates the CF ap- proach, and allows users to prove end-to-end theorems for higher-order imperative programs, from specification to language semantics, within a single theorem prover.

BibTeX Entry

  @inproceedings{Guneau_MKN_17,
    address          = {Uppsala, Sweden},
    author           = {Gu\'eneau, Armaël and Myreen, Magnus and Kumar, Ramana and Norrish, Michael},
    booktitle        = {European Symposium on Programming},
    month            = apr,
    pages            = {584--610},
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/9511.pdf},
    title            = {Verified Characteristic Formulae for {CakeML}},
    year             = {2017}
  }

Download