Reuse of proofs in software verification

DOI10.1007/BF02745521MaRDI QIDQ1419888zbMATH OpenFDO

Authors Wolfgang Reif, Kurt Stenzel

Publication date 27 January 2004

Published in Sādhanā (Search for Journal in Brave)

Full work available at URL https://www.ias.ac.in/describe/article/sadh/021/02/0229-0244

zbMATH Keywords

automated reuse of proofssoftware verification

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Flexible proof reuse for software verification
• Reuse in Software Verification by Abstract Method Calls
• Termination of theorem proving by reuse
• Proving theorems by reuse
• SETHEO goes software engineering: application of ATP to software reuse

Cites work

• First-order dynamic logic
• scientific article; zbMATH DE number 3702108 (Why is no real title available?)
• scientific article; zbMATH DE number 52140 (Why is no real title available?)
• scientific article; zbMATH DE number 3469999 (Why is no real title available?)
• Isabelle. A generic theorem prover
• Tactical theorem proving in program verification

Cited in

(10)

• Boosting the reuse of formal specifications
• Proving theorems by reuse
• Reusing predicate precision in value analysis
• Slicing techniques for verification re-use
• Deduction-based software component retrieval
• Mechanical proofs about computer programs
• scientific article; zbMATH DE number 4074538 (Why is no real title available?)
• Internal analogy in theorem proving
• Reuse in Software Verification by Abstract Method Calls
• Flexible proof reuse for software verification

Describes a project that uses

Uses Software

• Nuprl
• HOL
• Piton

This page was built for publication: Reuse of proofs in software verification

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1419888)