Accelerated Bounded Model Checking Using Interpolation Based Summaries

We propose a novel lazy bounded model checking (BMC) algorithm, Trace Inlining, that identifies relevant behaviors of the program to compute partial proofs as procedural summaries. Whenever procedures are reused in other contexts, Trace Inlining attempts to construct safety proofs using these summaries. If the current summaries are sufficient to complete the proof, it gains both in solving times and smaller encodings. If the summaries are found to be insufficient, they are automatically refined for future use. The partial proofs are enabled by a sequence of alternating underapproximation and overapproximation rounds until the program verification condition is found to be unsatisfiable. We evaluate our Trace Inlining algorithm on real-world benchmarks consisting of Windows and Linux device drivers. Our results show that the proposed algorithm is able to solve 12% additional benchmarks that were unsolved by state-of-the-art lazy BMC solvers CORRAL and LEGION. Further, Trace Inlining is 6x faster than CORRAL and 3x faster than LEGION in terms of verification time. The virtual best of all three verifiers is 4x faster than the virtual best of CORRAL and Legion, implying that our technique significantly improves on what is possible today.