Flexible Proof Reuse for Software Verification

Speaker: Chris Hunter (co-authors Peter Robinson, Paul Strooper)

When: 10:00, Monday, 21 June, 2004

Venue: 78-420

Proof reuse, or analogical reasoning, involves reusing the proof of a source theorem in the proof of a target conjecture. We have developed a method for proof reuse that is based on the generalisation --- replay paradigm described in the literature, in which a generalisation of the source proof is used to guide the construction of a target proof. This talk will provide an overview of our method, which includes a technique for producing more accurate source proof generalisations (using knowledge of the target goal), as well as a flexible replay strategy that allows the user to set various parameters to control the size and the shape of the search space. Finally, the results of applying this method to a case study from the realm of software verification will be presented.
 

Hospitality: Speaker (by default)

Contact: Prof Paul Bailes (SSE seminar co-ordinator) (p.bailes@epsa.uq.edu.au)

SSE seminar web page: http://www.itee.uq.edu.au/~sse/Seminars.html