Flexible proof reuse for software verification

Hunter, Chris, Robinson, Peter and Strooper, Paul (2004). Flexible proof reuse for software verification. In: C. Rattray, S. Maharaj and C. Shankland, Algebraic Methodology and Software Technology. The Tenth International Conference on Algebraic Methodology and Software Technology, Stirling, Scotland, (211-225). 12-16 July, 2004. doi:10.1007/b98770

Author Hunter, Chris
Robinson, Peter
Strooper, Paul
Title of paper Flexible proof reuse for software verification
Conference name The Tenth International Conference on Algebraic Methodology and Software Technology
Conference location Stirling, Scotland
Conference dates 12-16 July, 2004
Proceedings title Algebraic Methodology and Software Technology   Check publisher's open access policy
Journal name Algebraic Methodology and Software Technology: Proceedings   Check publisher's open access policy
Place of Publication Berlin
Publisher Springer-Verlag
Publication Year 2004
Year available 2004
Sub-type Fully published paper
DOI 10.1007/b98770
Open Access Status Not yet assessed
ISBN 3-540-22381-9
ISSN 0302-9743
Editor C. Rattray
S. Maharaj
C. Shankland
Volume 3116
Start page 211
End page 225
Total pages 15
Language eng
Abstract/Summary 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 replayed to construct the target proof. In this paper, we describe the novel aspects of our method, which include 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, we report on the results of applying this method to a case study from the realm of software verification.
Subjects E1
080399 Computer Software not elsewhere classified
080309 Software Engineering
Q-Index Code E1
Institutional Status UQ
Additional Notes Book Series: Lecture Notes in Computer Science

Version Filter Type
Citation counts: TR Web of Science Citation Count  Cited 0 times in Thomson Reuters Web of Science Article
Scopus Citation Count Cited 1 times in Scopus Article | Citations
Google Scholar Search Google Scholar
Created: Fri, 24 Aug 2007, 05:41:49 EST