Nicolas Klose

Abductive Inference of Separation Logic Specifications with Isorecursive User-Defined Predicates and Magic Wands

Program verifiers based on separation logic, such as Gillian, VeriFast, and Viper, allow one to prove complex properties of heap-manipulating, concurrent programs. These tools automate a large part of the proof search, but require a substantial amount of annotations such as metho...