Verification Condition Splitting

In a traditional approach to program verification, the correctness of

each procedure of a given program is encoded as a logical formula called the

verification condition. It is then up to a theorem prover, like an automatic SMT

solver, to analyze the verification condition in the attempt to either establish the

validity of the formula (thus proving the correct correct) or find counterexamples

In a traditional approach to program verification, the correctness of each procedure of a given program is encoded as a logical formula called the verification condition. It is then up to a theorem prover, like an automatic SMT solver, to analyze the verification condition in the attempt to either establish the validity of the formula (thus proving the correct correct) or find counterexamples (thus revealing errors in the program). This paper presents a technique that, via program-structure-aware transformations that split one verification condition up into several, lead to better overall performance of the SMT solver, sometimes making it up to several orders of magnitude faster. The technique also lends itself to improved error messages in case of verification failure due to time-outs.

VerificationConditionSplitting(Draft2008).pdf
PDF file

Publisher  Microsoft Research
© 2009 Microsoft Corporation. All rights reserved.

Details

TypeUnPublished
> Publications > Verification Condition Splitting