Tech Reports Home Contact
Technical Report Series
Submit Report
Browse Reports
Information for Authors
Contact Details

Technical Report HW-MACS-TR-0087

TitleVerification and Synthesis of Functional Correctness of Pointer Programs
AuthorsEwen Maclean, Andrew Ireland, Gudmund Grov
AbstractWe describe an approach to automatically reasoning about the functional correctness of pointer programs, in particular programs that involve iteration and recursion. Building upon separation logic, our approach has been implemented as a tightly integrated tool-chain ? where a novel combination of proof planning and invariant generation lies at its core. Starting from shape analysis, performed by the Smallfoot static analyzer, we use a proof plan called mutation to combine 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 Isa- Planner/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.


Email Technical Report's Administrator
|MACS Home| Top of the Page

Department of Computer Science, Heriot-Watt University, Riccarton, Edinburgh, EH14 4AS, +44 (0) 131 4514152

Last Updated: 02 September 2003 Copyright Heriot-Watt University, Disclaimer