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”.
Mon 15 Jul
|15:30 - 16:00|
|16:00 - 16:30|
|16:30 - 16:45|
Martin LesterUniversity of Reading
|16:45 - 17:00|