Skip to main content
Kent Academic Repository

Program Verification in the Presence of I/O

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. In: Verified Software. Theories, Tools, and Experiments. Lecture Notes in Computer Science . Springer. ISBN 978-3-030-03591-4. (doi:10.1007/978-3-030-03592-1_6) (KAR id:71298)

PDF (The final authenticated version is available online at https://doi.org/10.1007/978-3-030-03592-1_6) Author's Accepted Manuscript
Language: English
Download this file
(PDF/386kB)
[thumbnail of The final authenticated version is available online at https://doi.org/10.1007/978-3-030-03592-1_6]
Request a format suitable for use with assistive technology e.g. a screenreader
Official URL:
https://doi.org/10.1007/978-3-030-03592-1_6

Abstract

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: Book section
DOI/Identification number: 10.1007/978-3-030-03592-1_6
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Scott Owens
Date Deposited: 19 Dec 2018 15:53 UTC
Last Modified: 09 Dec 2022 06:42 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/71298 (The current URI for this page, for reference purposes)

University of Kent Author Information

Férée, Hugo.

Creator's ORCID:
CReDIT Contributor Roles:

Owens, Scott.

Creator's ORCID: https://orcid.org/0000-0002-7437-4780
CReDIT Contributor Roles:
  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.