2008 | OriginalPaper | Buchkapitel
Enhancing Program Verification with Lemmas
verfasst von : Huu Hai Nguyen, Wei-Ngan Chin
Erschienen in: Computer Aided Verification
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. 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.