{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T19:41:13Z","timestamp":1725565273568},"publisher-location":"Berlin, Heidelberg","reference-count":10,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540223818"},{"type":"electronic","value":"9783540278153"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-27815-3_19","type":"book-chapter","created":{"date-parts":[[2010,9,14]],"date-time":"2010-09-14T04:32:16Z","timestamp":1284438736000},"page":"211-225","source":"Crossref","is-referenced-by-count":0,"title":["Flexible Proof Reuse for Software Verification"],"prefix":"10.1007","author":[{"given":"Chris","family":"Hunter","sequence":"first","affiliation":[]},{"given":"Peter","family":"Robinson","sequence":"additional","affiliation":[]},{"given":"Paul","family":"Strooper","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"19_CR1","volume-title":"A Discipline of Programming","author":"E.W. Dijkstra","year":"1976","unstructured":"Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)"},{"key":"19_CR2","volume-title":"Essays in Computing Science","author":"C.A.R. Hoare","year":"1989","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. In: Hoare, C.A.R., Jones, C.B. (eds.) Essays in Computing Science, Prentice Hall, Englewood Cliffs (1989)"},{"key":"19_CR3","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1016\/0304-3975(75)90011-0","volume":"1","author":"G. Huet","year":"1975","unstructured":"Huet, G.: A unification algorithm for typed lambda-calculus. Theoretical Computer Science\u00a01, 27\u201357 (1975)","journal-title":"Theoretical Computer Science"},{"key":"19_CR4","first-page":"316","volume":"10","author":"E.B. Johnsen","year":"2003","unstructured":"Johnsen, E.B., L\u00fcth, C.: Abstracting transformations for refinement. Nordic Journal of Computing\u00a010, 316\u2013336 (2003)","journal-title":"Nordic Journal of Computing"},{"key":"19_CR5","volume-title":"Programming: The derivation of algorithms","author":"A. Kaldewaij","year":"1990","unstructured":"Kaldewaij, A.: Programming: The derivation of algorithms. Prentice Hall, Englewood Cliffs (1990)"},{"key":"19_CR6","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1007\/BFb0056323","volume-title":"Advances in Case-Based Reasoning","author":"E. Melis","year":"1998","unstructured":"Melis, E., Schairer, A.: Similarities and reuse of proofs in formal software verification. In: Smyth, B., Cunningham, P. (eds.) EWCBR 1998. LNCS (LNAI), vol.\u00a01488, pp. 76\u201387. Springer, Heidelberg (1998)"},{"key":"19_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"92","DOI":"10.1007\/3-540-61511-3_71","volume-title":"Automated Deduction - Cade-13","author":"E. Melis","year":"1996","unstructured":"Melis, E., Whittle, J.: Internal analogy in theorem proving. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol.\u00a01104, pp. 92\u2013105. Springer, Heidelberg (1996)"},{"key":"19_CR8","first-page":"135","volume":"5","author":"J. Reynolds","year":"1970","unstructured":"Reynolds, J.: Transformational systems and algebraic structure of atomic formulas. Machine Intelligence\u00a05, 135\u2013152 (1970)","journal-title":"Machine Intelligence"},{"key":"19_CR9","doi-asserted-by":"crossref","first-page":"194","DOI":"10.1112\/S1461157000000759","volume":"5","author":"M. Utting","year":"2002","unstructured":"Utting, M., Robinson, P., Nickson, R.: Ergo 6: a generic proof engine that uses Prolog proof technology. LMS Journal of Computation and Mathematics\u00a05, 194\u2013219 (2002)","journal-title":"LMS Journal of Computation and Mathematics"},{"issue":"1\u2013 2","key":"19_CR10","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1016\/S0004-3702(99)00096-X","volume":"116","author":"C. Walther","year":"2000","unstructured":"Walther, C., Kolbe, T.: Proving theorems by reuse. Artificial Intelligence\u00a0116(1\u2013 2), 17\u201366 (2000)","journal-title":"Artificial Intelligence"}],"container-title":["Lecture Notes in Computer Science","Algebraic Methodology and Software Technology"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-27815-3_19.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T03:27:56Z","timestamp":1620012476000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-27815-3_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540223818","9783540278153"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-27815-3_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}