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.