Amin Timany

Specifying I/O Using Abstract Nested Hoare Triples in Separation Logic

Willem Penninckx, Amin Timany, and Bart Jacobs: Specifying I/O Using Abstract Nested Hoare Triples in Separation Logic. In Proceedings of the 21st Workshop on Formal Techniques for Java-like Programs, July 2019. https://doi.org/10.1145/3340672.3341118

.pdf

Conference Paper

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},
}