2008 | OriginalPaper | Chapter
Enhancing Program Verification with Lemmas
Authors : Huu Hai Nguyen, Wei-Ngan Chin
Published in: Computer Aided Verification
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
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.