Verified characteristic formulae for CakeML
Authors
DATA61
Chalmers University of Technology
ENS de Lyon
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_2, address = {Uppsala}, author = {Gu\'{e}neau, Armaël and Myreen, Magnus and Kumar, Ramana and Norrish, Michael}, booktitle = {European Symposium on Programming}, date = {2017-4-22}, doi = {https://doi.org/10.1007/978-3-662-54434-1}, month = apr, pages = {584-610}, paperurl = {https://trustworthy.systems/publications/full_text/Guneau_MKN_17.pdf}, publisher = {Springer}, title = {Verified Characteristic Formulae for {CakeML}}, year = {2017} }