SMT: from Satisfiability to Optimization

Decanato - Facoltà di scienze informatiche

Data d'inizio: 24 Ottobre 2013

Data di fine: 25 Ottobre 2013

The Faculty of Informatics is pleased to announce a seminar given by Roberto Sebastiani

DATE: Thursday, October 24th 2013
PLACE: USI Lugano Campus, room SI-013, Informatics building (Via G. Buffi 13)
TIME: 09.30

ABSTRACT:
SMT solvers are widely used as workhorse engines in formal verification and many other applications. Many SMT-encodable problems, however, require solutions which are optimal wrt. some cost function. We call this problem, Optimization Modulo Theories (OMT).  In this talk I will first briefly introduce OMT; then I will present and discuss some work on OMT we have done in the recent years; finally, I will suggest challenges and research avenues.

BIO:
Roberto Sebastiani is Associate Professor at the Dipartimento di Ingegneria e Scienza dell'Informazione, University of Trento, Italy.

HOST: Prof. Natasha Sharygina