Mechanical proofs about computer programs

DOI10.1098/rsta.1984.0066zbMath0544.68012OpenAlexW2170606394MaRDI QIDQ3334054

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

specificationssoftware engineeringGypsy systemGypsy verification environmentmechanical proofs

Mathematics Subject Classification ID

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

Related Items (4)

Verification conditions for source-level imperative programs ⋮ The automated proof of a trace transformation for a bitonic sort ⋮ Problem-oriented verification system and its application to linear algebra programs ⋮ On the mechanical derivation of loop invariants

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