Efficient weakest preconditions

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.

tr-2004-34.pdf
PDF file

Details

TypeTechReport
NumberMSR-TR-2004-34
Pages11
InstitutionMicrosoft Research
> Publications > Efficient weakest preconditions