Simone Rollini successfully defended his doctoral thesis

 
Simone Rollini successfully defended his PhD thesis "Craig Interpolation and Proof Manipulation - Theory and Applications to Model Checking".
 
The full thesis can be downloaded here
 
 
Abstract:
 
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)