| Wiki Markup |
|---|
h1. 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.
...
._
h1. [Albert Oliveras|http://www.lsi.upc.edu/~oliveras/], Technical Univ. of Catalonia, Barcelona, Spain
{color:#333333}{_}Albert Oliveras has been doing research at the Technical _{color}
{color:#333333}{_}University of Catalonia (UPC) since 2002, where he is tenure-track _{color}
{color:#333333}{_}lecturer since 2007. He has a M.S in Mathematics (2002) and a PhD in _{color}
{color:#333333}{_}Computer Science (2006), both from UPC._{color}
{color:#333333}His research has been focused on developing theory, techniques and {color}
{color:#333333}{_}tools for SAT, SMT and decision procedures. He has been involved in _{color}
{color:#333333}{_}the implementation and design of the Barcelogic systems for SAT and _{color}
{color:#333333}{_}SMT, and the design of the MaxSAT solver MiniMaxSAT. These systems are _{color}
{color:#333333}{_}well-known for their efficiency and have won several awards at _{color}
{color:#333333}{_}different SAT, MaxSAT and SMT competitions. Recently, his primary _{color}
{color:#333333}{_}research interest has focused on applying SAT-based technology to solve _{color}
{color:#333333}{_}combinatorial optimization problems._{color}
{attachments:patterns=.*} |