OpenSMT and Applications: Lazy Abstraction, Interpolants, Proof Reduction

We describe OpenSMT and show its use (with demos) when applied to the Lazy-abstraction (with interpolants) framework, interpolants computation, interpolants strenght, and unsatisfiability-proof reduction.

Roberto Bruttomesso & Natasha Sharygina, University of Lugano, Lugano, Switzerland

Roberto received a M.S. Degree from the University of Milan (advisor S. Ghilardi), in 2004, and a Doctoral Degree from the University of Trento (advisor A. Cimatti), in 2008. Currently he is a Post-Doc in the Formal Verification Group at the University of Lugano. His main research interests include decision procedures and in particular satisfiability modulo theories applied to model checking for the verification of hardware and software.

-----------------------------------------------------------------------------

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 research has been funded by multiple grants including the CMU SEI Independent R&D grants, Tasso Career, the Swiss National Foundation, and European Union Research grants. Prof. Sharygina has authored more than 55 research papers in areas of formal verification, and system design. She served on program committees of various conferences (e.g., TACAS, FMCAD, CAV), given keynote and invited presentations, and co-chaired several 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.