Specifying I/O Using Abstract Nested Hoare Triples in Separation Logic
DOI
Keywords: input/output, modular program verification, module specifications, separation logic
Abstract.
We propose a separation logic-based approach for modular specification and verification of the I/O behavior of a program. The approach uses higher-order separation logic predicates to express abstract nested Hoare triples that abstractly associate a precondition and a postcondition with an I/O action. The approach supports verifying higher-level I/O actions built on top of lower-level ones (e.g. the I/O abstractions offered by the programming language''s standard library, implemented on top of system calls), as well as virtual I/O actions that in fact only manipulate memory, against specifications that are indistinguishable from those of the "primitive I/O actions".
The bibtex source for this publication:
@inproceedings{Penninckx:2019:SIU:3340672.3341118,
author = {Penninckx, Willem and Timany, Amin and Jacobs, Bart},
title = {Specifying I/O Using Abstract Nested Hoare Triples in Separation Logic},
booktitle = {Proceedings of the 21st Workshop on Formal Techniques for Java-like Programs},
series = {FTfJP ''19},
year = {2019},
isbn = {978-1-4503-6864-3},
location = {London, United Kingdom},
pages = {5:1--5:7},
articleno = {5},
numpages = {7},
url = {http://doi.acm.org/10.1145/3340672.3341118},
doi = {10.1145/3340672.3341118},
acmid = {3341118},
publisher = {ACM},
address = {New York, NY, USA},
keywords = {input/output, modular program verification, module specifications, separation logic},
}