Craig Interpolation and Proof Manipulation - Theory and Applications to Model Checking

Decanato - Facoltà di scienze informatiche

Data d'inizio: 23 Ottobre 2013

Data di fine: 24 Ottobre 2013

You are cordially invited to attend the PhD Dissertation Defense of Simone Fulvio ROLLINI on Wednesday, October 23rd 2013 at 15h00 in room CC-351 (main building)

Symbolic model checking has been considerably enhanced  with the introduction of Craig interpolation as a means of overapproximation. Interpolants, usually generated from proofs of unsatisfiability, are not unique, and it is an open problem to understand which interpolants have the highest quality, resulting in an optimal verification performance.

The goal of this research 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.

Dissertation Committee:

  • Prof. Natasha Sharygina, Università della Svizzera italiana, Switzerland (Research Advisor)
  • Prof. Rolf Krause, Università della Svizzera italiana, Switzerland (Internal Member)
  • Prof. Evanthia Papadopoulou, Università della Svizzera italiana, Switzerland (Internal Member)
  • Prof. Roberto Sebastiani, Università di Trento, Italy (External Member)
  • Prof. Ofer Strichman, Technion, Israel (External Member)