Mechanical proofs about computer programs

DOI10.1098/RSTA.1984.0066MaRDI QIDQ3334054zbMATH OpenOpenAlexFDO

Authors Donald I. Good

Publication date 1984

Published in Philosophical Transactions of the Royal Society of London. Series A, Mathematical and Physical Sciences (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1098/rsta.1984.0066

zbMATH Keywords

software engineeringspecificationsGypsy systemGypsy verification environmentmechanical proofs

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Theory of software (68N99)

Recommendations

• Proofs verifying programs and programs producing proofs: a conceptual analysis
• Program verification. Fundamental issues in computer science
• Reuse of proofs in software verification
• scientific article; zbMATH DE number 4172362
• scientific article; zbMATH DE number 3858384

Cited in

(7)

• Theories for mechanical proofs of imperative programs
• A machine program for theorem-proving
• scientific article; zbMATH DE number 2102718 (Why is no real title available?)
• Verification conditions for source-level imperative programs
• On the mechanical derivation of loop invariants
• Problem-oriented verification system and its application to linear algebra programs
• The automated proof of a trace transformation for a bitonic sort

This page was built for publication: Mechanical proofs about computer programs

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