Program Verification


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.

Download options


    Upload a copy of this work     Papers currently archived: 72,660

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.


Added to PP

26 (#443,743)

6 months
1 (#388,784)

Historical graph of downloads
How can I increase my downloads?

Similar books and articles

Program Verification: The Very Idea.James H. Fetzer - 1988 - Communications of the Acm 31 (9):1048--1063.
Metamathematics, Machines and Gödel's Proof.N. Shankar - 1994 - Cambridge University Press.
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.