Modular Total Correctness Verification of Fine-Grained Concurrent Programs with Exceptions and I/O

Опубликовано 21 июня 2016, 23:26

Many powerful higher-order logics have been proposed for the modular specification and verification of fine-grained concurrent imperative programs. In this talk, I present a logic that is fairly close to what my VeriFast modular verification tool for C and Java implements. To achieve higher-order-ishness (higher-order assertions, nested Hoare triples, storing assertions in the heap, etc.), a relatively simple approach is followed: assertion lambda applications and nested triples may occur only in positive positions. Negative facts can be passed around in the form of lemma lambdas, i.e. ghost command lambdas. We prove termination of such higher-order ghost code using call permissions, a technique we are presenting at ECOOP 2015 this summer. I will also discuss the problem of provably live exception handling (FTfJP 2015), and modular verification of interactive behavior (ESOP 2014).