Modular formal specification and verification of complex imperative modules such as fine-grained concurrent algorithms requires the use of a powerful, higher-order program logic. Approaches currently being proposed in the literature, such as Iris [Jung et al., POPL 2015], are based on guarded recursion using the “later” operator. Our VeriFast tool for modular formal verification of C and Java programs uses a somewhat different approach, based on a positivity restriction [Parkinson and Bierman, POPL 2005] and the use of higher-order ghost code combined with a general modular termination verification approach [Jacobs et al., ECOOP 2015] to encode non-positive constructs. In this poster presentation we present a formalization and soundness proof outline, as well as examples of the use (based on Jacobs and Piessens [POPL 2011]) of our approach.

Assistant professor at the iMinds-DistriNet research group at the Department of Computer Science, KU Leuven - University of Leuven, Belgium