Mutation in Linked Data Structures

Ewen Maclean, Andrew Ireland

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


Separation logic was developed as an extension to Hoare logic with the aim of simplifying pointer program proofs. A key feature of the logic is that it focuses the reasoning effort on only those parts of the heap that are relevant to a program - so called local reasoning. Underpinning this local reasoning are the separating conjunction and separating implication operators. Here we present an automated reasoning technique called mutation that provides guidance for separation logic proofs. Specifically, given two heap structures specified within separation logic, mutation attempts to construct an equivalence proof using a difference reduction strategy. Pivotal to this strategy is a generalised decomposition operator which is essential when matching heap structures. We show how mutation provides an effective strategy for proving the functional correctness of iterative and recursive programs within the context of weakest precondition analysis. Currently, mutation is implemented as a proof plan within our CORE program verification system. CORE combines results from shape analysis with our work on invariant generation and proof planning. We present our results for mutation within the context of the CORE system.
Original languageEnglish
Title of host publicationFormal Methods and Software Engineering
Subtitle of host publication13th International Conference on Formal Engineering Methods, ICFEM 2011, Durham, UK, October 26-28, 2011. Proceedings
Place of PublicationBerlin, Heidelberg
PublisherSpringer Berlin Heidelberg
Number of pages16
ISBN (Print)978-3-642-24558-9
Publication statusPublished - 2011

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
ISSN (Print)0302-9743


Dive into the research topics of 'Mutation in Linked Data Structures'. Together they form a unique fingerprint.

Cite this