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.