Verification Condition Splitting

K. Rustan M. Leino, Michal Moskal, and Wolfram Schulte

2008

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.

PDF file |

Publisher Microsoft Research

© 2009 Microsoft Corporation. All rights reserved.

Type | UnPublished |

> Publications > Verification Condition Splitting