Proof automation for functional correctness in separation logic

Ewen Maclean, Andrew Ireland, Gudmund Grov

Research output: Contribution to journalArticle

1 Citation (Scopus)
37 Downloads (Pure)

Abstract

We describe an approach to automatically prove the functional correctness of pointer programs that involve iteration and recursion. Building upon separation logic, our approach has been implemented as a tightly integrated tool chain incorporating a novel combination of proof planning and invariant generation. Starting from shape analysis, performed by the Smallfoot static analyser, we have developed a proof strategy that combines shape and functional aspects of the verification task. By focusing on both iterative and recursive code, we have had to address two related invariant generation tasks, i.e. loop and frame invariants. We deal with both tasks uniformly using an automatic technique called term synthesis, in combination with the IsaPlanner/Isabelle theorem prover. In addition, where verification fails, we attempt to overcome failure by automatically generating missing preconditions. We present in detail our experimental results. Our approach has been evaluated on a range of examples, drawn in part from a functional extension to the Smallfoot corpus.

Original languageEnglish
Pages (from-to)641-675
Number of pages35
JournalJournal of Logic and Computation
Volume26
Issue number2
Early online date28 May 2014
DOIs
Publication statusPublished - Apr 2016

Keywords

  • Proof planning
  • functional correctness
  • invariant discovery
  • separation logic
  • substructural logic
  • automated theorem proving
  • LINEAR LOGIC
  • SMALLFOOT

Cite this