Back
Texte intégral
Doctoral thesis

Craig Interpolation and proof manipulation : Theory and applications to model checking

    23.10.2013

204 p

Thèse de doctorat: Università della Svizzera italiana, 2013

Formal verification
Model checking
Craig interpolation
Proof theory
Proof transformation
Satisfiability
English 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 reduce the size of interpolants generated from them. Finally, we provide experimental evidence that size and logical strength have a significant impact on verification: small interpolants improve the verification performance, while stronger or weaker interpolants are beneficial in different model checking applications. Interpolants are generated from proofs, as produced by logic solvers. As a secondary line of research, we developed and successfully tested a hybrid propositional satisfiability solver built on a model-based stochastic technique known as cross-entropy method.
Language
  • English
Classification
Computer science and technology
License
License undefined
Identifiers
Persistent URL
https://n2t.net/ark:/12658/srd1318391
Statistics
Document views: 66 File downloads:
  • 2013INFO006.pdf: 50