Inductive reasoning for shape invariants

Lilia Georgieva, Patrick Maier

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

Abstract

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
Pages75-89
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

Conference

ConferenceInternational Workshop on First-Order Theorem Proving, FTP 2009
CountryNorway
CityOslo
Period6/07/097/11/12

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

  • Cite this

    Georgieva, L., & Maier, P. (2009). Inductive reasoning for shape invariants. In N. Peltier, & V. Sofronie-Stokkermans (Eds.), Proceedings of the 7th International Workshop on First-Order Theorem Proving (FTP'09) (pp. 75-89). University of Oslo. http://ceur-ws.org/Vol-556/paper08.pdf