Inductive reasoning for shape invariants

Lilia Georgieva, Patrick Maier

Research output: Chapter in Book/Report/Conference proceedingConference contribution


Automatic verification of imperative programs that destructively manipulate heap data structures is challenging. In this paper we propose an approach for verifying that such programs do not corrupt their data structures. We specify heap data structures such as lists, arrays of lists, and trees inductively as solutions of logic programs. We use off-the-shelf first-order theorem provers to reason about these specifications.
Original languageEnglish
Title of host publicationProceedings of the 7th International Workshop on First-Order Theorem Proving (FTP'09)
EditorsNicolas Peltier, Viorica Sofronie-Stokkermans
Place of PublicationOslo
PublisherUniversity of Oslo
Number of pages15
ISBN (Print)82-7368-347-8
Publication statusPublished - Jul 2009
EventInternational Workshop on First-Order Theorem Proving, FTP 2009 - Oslo, Norway
Duration: 6 Jul 20097 Nov 2012


ConferenceInternational Workshop on First-Order Theorem Proving, FTP 2009


Dive into the research topics of 'Inductive reasoning for shape invariants'. Together they form a unique fingerprint.

Cite this