Skip to main content

Program verification in the presence of I/O: semantics, verified library routines, and verified applications


Hugo Feree, Johannes Åman Pohjola, Ramana Kumar, Scott Owens, Magnus Myreen and Son Ho

University of Kent


École Polytechnique

Chalmers University of Technology

UNSW Sydney


Software verification tools that build machine-checked proofs of functional correctness usually focus on the algorithmic content of the code. Their proofs are not grounded in a formal semantic model of the environment that the program runs in, or the program’s interaction with that environment. As a result, several layers of translation and wrapper code must be trusted. In contrast, the CakeML project focuses on end-to-end verification to replace this trusted code with verified code in a cost-effective manner. In this paper, we present infrastructure for developing and verifying impure functional programs with I/O and imperative file handling. Specifically, we extend CakeML with a low-level model of file I/O, and verify a high-level file I/O library in terms of the model. We use this library to develop and verify several Unix-style command-line utilities: cat, sort, grep, diff and patch. The workflow we present is built around the HOL4 theorem prover, and therefore all our results have machine-checked proofs.

BibTeX Entry

    publisher        = {Springer},
    booktitle        = {Verified Software: Theory, Tools and Experiments},
    month            = nov,
    paperurl         = {},
    year             = {2018},
    volume           = {11294},
    title            = {Program Verification in the Presence of {I}/{O}: Semantics, verified library routines, and verified
    pages            = {88-111},
    author           = {Feree, Hugo and {\AA}man Pohjola, Johannes and Kumar, Ramana and Owens, Scott and Myreen, Magnus and
                        Ho, Son},
    address          = {Oxford, UK},
    date             = {2018-11-24}