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

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".

ISBN:978-1-4503-6864-3

Publication year:2019

BOF-keylabel:yes

IOF-keylabel:yes

Authors from:Higher Education

Accessibility:Open