|
|
Technical Report HW-MACS-TR-0087
| Title | Verification and Synthesis of Functional Correctness of Pointer Programs |
|---|
| Authors | Ewen Maclean, Andrew Ireland, Gudmund Grov |
|---|
| Date | 2011-04-12 |
|---|
| Abstract | We 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. |
|---|
| Group | DSG |
|---|
| Notes | |
|---|
| Download |   |
|---|
|
|
