• Created by Unknown User (leberre_1@touchstonenetwork.net), last modified by Unknown User (roberto.bruttomesso_1@touchstonenetwork.net) on May 18, 2011 07:59

You are viewing an old version of this page. View the current version.

Compare with Current View Page History

« Previous Version 6 Next »

OpenSMT and Applications

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.

  • No labels