Seminars

Local proof transformations for flexible interpolation and proof reduction  PDF files
Natasha Sharygina - University of Lugano, Formal Verification and Security Lab

06/20/2011, 2pm, GHC-8102

Abstract

Model checking based on Craig's interpolants ultimately relies on efficient engines, such as SMT-Solvers, to log proofs of unsatisfiability and to derive the desired interpolant by means of a set of algorithms known in literature. These algorithms, however, are designed for proofs that do not contain mixed predicates. In this talk I will present a technique for transforming the propositional proof produced by an SMT-Solver in such a way that mixed predicates are eliminated. There exists a number of cases in which mixed predicates arise as a consequence of state-of-the-art solving procedures (e.g., lemma on demand, theory combination, etc.). In such cases our technique can be applied to allow the reuse of known interpolation algorithms. I will then present a new approach to proof reduction, situated among the purely post-processing methods. The main idea is to reduce the proof size by eliminating redundancies of occurrences of pivots along the proof paths. This is achieved by matching and rewriting local contexts into simpler ones. In our approach, rewriting can be easily customized in the way local contexts are matched, in the amount of transformations to be performed, or in the different application of the rewriting rules. I will provide experimental evaluation of our technique on a set of SMT and SAT benchmarks, which shows considerable reduction in the proofs size.

Biography

Natasha Sharygina is a Professor of Informatics at the University of Lugano, Switzerland and an adjunct Professor at School of Computer Science, Carnegie Mellon University, Pittsburgh, USA. Prof. Sharygina received a Ph.D. degree from the University of Texas at Austin, USA in 2002. Her professional experience includes consulting at Bell Labs, Lucent Technologies at the Computing Sciences Research in 2000-2001 and a research faculty position at Carnegie Mellon University, SEI in 2002-2005.

Prof. Sharygina directs the USI Formal Verification and Security group whose research deals with improving the program development process through formal methods of specification and verification. Prof. Sharygina´s interests lie in software and hardware verification, temporal logics, model checking, SAT/ SMT methods, and concurrent and distributed computing. Prof. Sharygina’s current focus is on applying automated formal methods to problems in computer security, electronic design automation, and program analysis.

Prof. Sharygina is the recipient of various awards among which are the ACM recognition of service award and CMU Technical Excellence awards.

Prof. Sharygina’s research has been funded by multiple grants including the CMU SEI Independent R&D grants, European Union FP7 (Pincette) and COST (Richmodels)  projects,  and awards from Tasso, Swiss National Science, and Hasler Foundations. Prof. Sharygina has authored more than 60 research papers in areas of formal verification, and system design. She served on program committees of various conferences (e.g., TACAS, FMCAD, CAV, SPIN), given keynote and invited presentations, and co-chaired several conferences and workshops in the area of formal verification. Prof. Sharygina is chairing FMCAD 2010 and CAV 2013, the major conferences in computer-aided verification and design.