Craig Interpolation and proof manipulation
Simone Fulvio Rollini · 2013
Model checking is one of the most appreciated methods for automated formal verification of software and hardware systems. The main challenge in model checking, i.e. scalability to complex systems of extremely large size, has been successfully addressed by means of symbolic techniques, which rely on an efficient representation and manipulation of the systems based on first order logic. Symbolic model checking has been considerably enhanced with the introduction in the last years of Craig interpolation as a means of overapproximation. Interpolants can be efficiently computed from proofs of unsatisfiability based on their structure. A number of algorithms are available to generate different interpolants from the same proof; additional interpolants can be obtained by turning a proof into another proof of unsatisfiability of the same formula using transformation techniques. Interpolants are thus not unique, and it is fundamental to understand which interpolants have the highest quality, resulting in an optimal verification performance; it is an open problem to determine what features determine the quality of interpolants, and how they are connected with the effectiveness in verification. The goal of this thesis is to identify aspects that make interpolants good, and to develop new techniques that guide the generation of interpolants in order to improve the performance of model checking approaches. We contribute to the state-of-the-art by providing a characterization of quality in terms of semantic and syntactic features, such as logical strength, size, presence of quantifiers. We present a family of algorithms that generalize existing techniques and are able to produce interpolants of different structure and strength, with and without quantifiers, from the same proof. These algorithms are examined in the context of various model checking applications, where collections of interdependent interpolants satisfying particular properties are needed; we formally analyze the relationships among the properties and derive necessary and sufficient conditions on the applicability of the algorithms. We introduce a framework for proof manipulation; it includes a method to overcome limitations in existing interpolation algorithms for first order theories, as well as a set of compression algorithms, which, reducing the size of proofs, consequently