SMT Theory and DPLL(T)

This talk will present a basic overview of SMT, focusing on the DPLL(T) 
approach.  We will review the most interesting theories that SMT 
solvers can deal with and will introduce the basic ingredients of a 
DPLL(T)-based SMT solver.

Albert Oliveras, Technical Univ. of Catalonia, Barcelona, Spain

Albert Oliveras has been doing research at the Technical 
University of Catalonia (UPC) since 2002, where he is tenure-track 
lecturer since 2007. He has a M.S in Mathematics (2002) and a PhD in 
Computer Science (2006), both from UPC.

His research has been focused on developing theory, techniques and 
tools for SAT, SMT and decision procedures. He has been involved in 
the implementation and design of the Barcelogic systems for SAT and 
SMT, and the design of the MaxSAT solver MiniMaxSAT. These systems are 
well-known for their efficiency and have won several awards at 
different SAT, MaxSAT and SMT competitions. Recently, his primary 
research interest has focused on applying SAT-based technology to solve 
combinatorial optimization problems.