Proof and the computer: some issues raised by the formal verification of computer systems

Donald MacKenzie

Science and Public Policy, 1996, vol. 23, issue 1, 45-53

Abstract: Formal verification is the attempt to give a mathematical proof that the design of a computer system is a correct implementation of its specification. This effort raises questions about what ‘proof’ is. Two main conceptions — formal proof and rigorous argument — are identified, and it is suggested that they are underpinned by the disciplinary authorities, respectively, of logic and mathematics. The views of specialists in formal verification about the degree of certainty that can be claimed for verification are examined, and it is argued that the temptations to claims of certainty unwittingly offered by the commercial and regulatory environment must be resisted Copyright , Beech Tree Publishing.

Date: 1996
References: Add references at CitEc
Citations:

Downloads: (external link)
http://hdl.handle.net/10.1093/spp/23.1.45 (application/pdf)
Access to full text is restricted to subscribers.

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:oup:scippl:v:23:y:1996:i:1:p:45-53

Access Statistics for this article

Science and Public Policy is currently edited by Nicoletta Corrocher, Jeong-Dong Lee, Mireille Matt and Nicholas Vonortas

More articles in Science and Public Policy from Oxford University Press
Bibliographic data for series maintained by Oxford University Press ().