AbstractHow 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.
Added to PP
Historical graph of downloads
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
Is “Some-Other-Time” Sometimes Better Than “Sometime” for Proving Partial Correctness of Programs?Ildikó Sain - 1988 - Studia Logica 47 (3):279 - 301.
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 - 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.
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 - Department of Computer Science, University of Illinois at Urbana-Champaign.
References found in this work
Prolegomena to a Theory of Mechanized Formal Reasoning.Richard W. Weyhrauch - 1980 - Artificial Intelligence 13 (1-2):133-170.
An Experimental Program Transformation and Synthesis System.John Darlington - 1981 - Artificial Intelligence 16 (1):1-46.
Citations of this work
No citations found.