Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Efficient weakest preconditions

K. Rustan M. Leino


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. The new understanding of this technique spotlights the program property that makes the technique work.


Publication typeTechReport
InstitutionMicrosoft Research
> Publications > Efficient weakest preconditions