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.
Keywords No keywords specified (fix it)
Categories No categories specified
(categorize this paper)
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

Our Archive

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 41,553
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library

References found in this work BETA

Add more references

Citations of this work BETA

No citations found.

Add more citations

Similar books and articles

Program Verification: The Very Idea.James H. Fetzer - 1988 - Communications of the Acm 31 (9):1048--1063.
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.


Added to PP index

Total views
25 ( #331,274 of 2,248,940 )

Recent downloads (6 months)
2 ( #795,491 of 2,248,940 )

How can I increase my downloads?


My notes

Sign in to use this feature