Program Verification

&

Abstract

How are the properties of computer programs proved? We discuss three approaches in this article: inductive invariants, functional semantics, and explicit semantics. Because the first approach has received by far the most attention, it has produced the most impressive results to date. However, the field is now moving away from the inductive invariant approach.

Categories

Add categories

Keywords

Reprint years

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 92,923

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

  • Only published works are available at libraries.

My notes

Similar books and articles

Program verification: the very idea.James H. Fetzer - 1988 - Communications of the Acm 31 (9):1048--1063.
Program verification, defeasible reasoning, and two views of computer science.Timothy R. Colburn - 1991 - Minds and Machines 1 (1):97-116.
Deductive program verification (a practitioner's commentary).David A. Nelson - 1992 - Minds and Machines 2 (3):283-307.
The use of a formal simulator to verify a simple real time control program.Robert Boyer - manuscript
Metamathematics, machines, and Gödel's proof.N. Shankar - 1994 - New York: Cambridge University Press.
Is “some-other-time” sometimes better than “sometime” for proving partial correctness of programs?Ildikó Sain - 1988 - Studia Logica 47 (3):279 - 301.
Adventures in the verification of mathematics.Harvey Friedman - manuscript
Program Verification and Functioning of Operative Computing Revisited: How about Mathematics Engineering? [REVIEW]Uri Pincas - 2011 - Minds and Machines 21 (2):337-359.
Experimental Methods for Unraveling the Mind-body Problem: The Phenomenal Judgment Approach.Victor Argonov - 2014 - Journal of Mind and Behavior 35 (1-2):51-70.
The uniclass inductive program AQ7UNI: program implementation and user's guide.Robert Stepp - 1979 - Urbana, Ill.: Dept. of Computer Science, University of Illinois at Urbana-Champaign.
Inductive countersupport.Georg J. W. Dorn - 1995 - Journal for General Philosophy of Science / Zeitschrift für Allgemeine Wissenschaftstheorie 26 (1):187 - 189.
A Program for Computational Semantics.Jan van Eijck - unknown
Program semantics and classical logic.Reinhard Muskens - 1997) - In CLAUS Report Nr 86. Saarbrücken: University of the Saarland. pp. 1-27.
YAQ: a 360 assembler version of the algorithm Aq and comparison with other PL/I programs.Edward Yalow - 1977 - Urbana: Department of Computer Science, University of Illinois at Urbana-Champaign.
O związkach informatyki z matematyką.Izabela Bondecka-Krzykowska - 2010 - Filozofia Nauki 18 (1).

Analytics

Added to PP
2010-12-22

Downloads
32 (#514,490)

6 months
6 (#585,724)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

No citations found.

Add more citations

References found in this work

Prolegomena to a theory of mechanized formal reasoning.Richard W. Weyhrauch - 1980 - Artificial Intelligence 13 (1-2):133-170.

Add more references