Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
10331424 | Information Processing Letters | 2005 | 8 Pages |
Abstract
Desired computer-program properties can be described by logical formulas called verification conditions. Different mathematically-equivalent forms of these verification conditions can have a great impact on the performance of an automatic theorem prover that tries to discharge them. This paper presents a simple weakest-precondition understanding of the ESC/Java technique for generating verification conditions. This new understanding of the technique spotlights the program property that makes the technique work.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
K. Rustan M. Leino,