Program Verification in the Presence of I/O - Semantics, Verified Library Routines, and Verified Applications

Férée, Hugo and Pohjola, Johannes Aman and Kumar, Ramana and Owens, Scott and Myreen, Magnus O. and Ho, Son (2018) Program Verification in the Presence of I/O - Semantics, Verified Library Routines, and Verified Applications. In: 10th International Conference on Verified Software: Theories, Tools, and Experiments. (doi: (Full text available)

PDF (The final authenticated version is available online at - Author's Accepted Manuscript
Download (322kB) Preview
Official URL


Software veri?cation 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 endto-end veri?cation to replace this trusted code with veri?ed code in a cost-e?ective manner. In this paper, we present infrastructure for developing and verifying impure functional programs with I/O and imperative ?le handling. Specifically, we extend CakeML with a low-level model of ?le I/O, and verify a high-level ?le 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, di? and patch. The work?ow we present is built around the HOL4 theorem prover, and therefore all our results have machine-checked proofs.

Item Type: Conference or workshop item (Paper)
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Faculties > Sciences > School of Computing > Programming Languages and Systems Group
Depositing User: Scott Owens
Date Deposited: 19 Dec 2018 15:53 UTC
Last Modified: 03 Jan 2019 16:46 UTC
Resource URI: (The current URI for this page, for reference purposes)
  • Depositors only (login required):


Downloads per month over past year