Enhancing Program Verification with Lemmas

摘要

One promising approach to verifying heap-manipulating programs is based on user-defined inductive predicates in separation logic. This approach can describe data structures with complex invariants and sound reasoning based on unfold/fold. However, an important component towards more expressive program verification is the use of lemmas that can soundly relate predicates beyond their original definitions. This paper outlines a new automatic mechanism for proving and applying user-specified lemmas under separation logic.