Optimizing Function Summaries Through Interpolation

Abstract

Two of the static analysis techniques presented in this book use Craig interpolation, a means of over-approximation, to achieve efficient SAT-based symbolic model checking. Different verification applications exploit interpolants for different purposes; it is unlikely that a single interpolation procedure could provide interpolants fit for all cases. This chapter describes the PeRIPLO framework, an interpolating SAT solver that implements a set of techniques to generate and manipulate interpolants for different model-checking tasks. Even though the PeRIPLO framework can be used for many other purposes besides static analysis, we will use it to illustrate in an interesting way the benefits and challenges of Craig-interpolation-based Bounded Model Checking. We demonstrate the flexibility of the framework in two software bounded model checking applications described in Chaps. 5 and 6: verification of a given source code incrementally with respect to various properties, and verification of software upgrades with respect to a fixed set of properties. Both applications use interpolation for generating function summaries. Our systematic experimental investigation shows that the size and logical strength of interpolants significantly affect verification, and that these characteristics depend on the role interpolants play in the verification process. The chapter is based on the research previously published in [RAF+13].