Albert Oliveras i Llunell

Assistant professor (professor lector)
Technical University of Catalonia
LSI Department, Building Omega, room 114
Jordi Girona 1
E-08034 Barcelona
SPAIN
E-mail: oliveras AT(NSPAM) lsi.upc.edu
Phone: (34) 93 413 77 92
Fax: (34) 93 413 78 33

Education:

PhD. in Computer Science (defended July 2006), Department LSI at UPC.
[Slides]
M.S. in Mathematics (1997-2002), School of Mathematics and Statistics (FME) at UPC.

Research:

The research developed by our group is related to Logic in Computer Science. More specifically, I have worked on:

SAT
Satisfiability Modulo Theories
Domain-specific decision procedures
Automated theorem proving
Implementation of logics

Professional activities:

PC member for the 6th International Workshop on the Implemenetation of Logics , November 12th, 2006. Phnom Penh (Cambodia).
Programme committe co-chair of the 5th International Workshop on Satisfiability Modulo Theories (SMT 2007) (successor of PDPAR). July 1-2, 2007. Berlin (Germany).
PC member for the 21st International Conference on Automated Deduction (CADE-21). July 17-20, 2007. Bremen (Germany).
PC member for the 6th International Workshop on Frontiers of Combining Systems (FroCoS 2007). September 2007. Liverpool (United Kingdom).
Co-organizer of the 3rd International Satisfiability Modulo Theories Competition (SMT-COMP 2007). July 3-7, 2007. Berlin (Germany).
PC member for the 1st Workshop on Practical Aspects of Automated Reasoning (PAAR'08). August 2008. Sidney (Australia).
PC member for the 7th International Workshop on the Implemenetation of Logics , November 2008. Doha (Qatar).
PC member for the 22nd International Conference on Automated Deduction, August 2009. Montreal (Canada).
PC member for the 7th International Workshop on Frontiers of Combining Systems (FroCoS 2009). September 2009. Trento (Italy).
PC member for the 12th International Conference on Theory and Applications of Satisfiability Testing (SAT 2009). July 2009. Swansea (United Kingdom).

Publications (in reverse chronological order):

JOURNAL ARTICLES:

"MiniMaxSAT: An efficient Weighted Max-SAT Solver"
Federico Heras, Javier Larrosa, Albert Oliveras.
Journal of Artificial Intelligence Research (JAIR), 31:1-32, January 2008.
[ Paper | BibTeX ]
"Design and Results of the 3rd Annual Satisfiability Modulo Theories Competition (SMT-COMP'07)"
Clark Barrett, Morgan Deters, Albert Oliveras, Aaron Stump.
International Journal on Artificial Intelligence Tools (IJAIT). To appear.
"Fast Congruence Closure and Extensions"
Robert Nieuwenhuis, Albert Oliveras.
Information and Computation, 205(4):557-580, April 2007.
[ Paper | BibTeX ]
"Solving SAT an SAT Modulo Theories: from an Abstract Davis-Putnam-Logemann-Loveland Procedure to DPLL(T)"
Robert Nieuwenhuis, Albert Oliveras and Cesare Tinelli.
Journal of the ACM, 53(6), 937-977, November 2006.
[ Paper | BibTeX ]

CONFERENCE PAPERS:

"Efficient Generation of Unsatisfiability Proofs and Cores in SAT"
Roberto Asín, Robert Nieuwenhuis, Albert Oliveras and Enric Rodríguez-Carbonell.
15th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR). November 2008, Doha (Qatar).
[ Paper ]
"A Write-Based Solver for SAT Modulo the Theory of Arrays"
Miquel Bofill, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell and Albert Rubio
Formal Methods in Computer-Aided Design 2008 (FMCAD), November 2008, Portland (USA).
[ Paper ]
"The Barcelogic SMT Solver"
Miquel Bofill, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell and Albert Rubio
20th International Conference on Computer Aided Verification (CAV), July 2008, Princeton (USA).
[ Paper | BibTeX ]
"SAT Modulo the Theory of Linear Arithmetic: Exact, Inexact and Commercial Solvers"
Germain Faure, Robert Nieuwenhuis, Albert Oliveras and Enric Rodríguez-Carbonell
11th International Conference on Theory and Applications of Satisfiability Testing (SAT). May 2008, Guangzhou (China).
[ Paper | Slides | BibTeX ]
"Challenges in Satisfiability Modulo Theories (Invited Paper)"
Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell and Albert Rubio
18th International Conference on Rewriting Techniques and Applications (RTA). June 2007, Paris (France).
[ Paper | BibTeX ]
"MiniMaxSat: a New Weighted Max-SAT Solver"
Federico Heras, Javier Larrosa and Albert Oliveras.
10th International Conference on Theory and Applications of Satisfiability Testing (SAT). May 2007, Lisbon (Portugal).
[ Paper | BibTeX ]
"Splitting on Demand in Satisfiability Modulo Theories"
Clark Barrett, Robert Nieuwenhuis, Albert Oliveras and Cesare Tinelli.
13th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR). November 2006, Phnom Penh (Cambodia).
[ Paper | Slides | BibTeX ]
"On SAT Modulo Theories and Optimization Problems"
Robert Nieuwenhuis and Albert Oliveras.
9th International Conference on Theory and Applications of Satisfiability Testing (SAT), August 2006, Seattle (USA).
[ Paper | BibTeX ]
"SMT Techniques for Fast Predicate Abstraction"
Shuvendu K. Lahiri, Robert Nieuwenhuis and Albert Oliveras.
18th International Conference on Computer Aided Verification (CAV), August 2006, Seattle (USA).
[ Paper | Slides | BibTeX ]
"Decision procedures for SAT, SAT Modulo Theories and Beyond. The BarcelogicTools. (Invited Paper)"
Robert Nieuwenhuis, Albert Oliveras.
12th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR). December 2005, Montego Bay (Jamaica).
[ Paper | BibTeX ]
"DPLL(T) with Exhaustive Theory Propagation and its Application to Difference Logic"
Robert Nieuwenhuis, Albert Oliveras.
17th International Conference on Computer Aided Verification (CAV), July 2005, Edinburgh (Scotland).
[ Paper | Detailed experimental results | BibTeX ]
"Proof-producing Congruence Closure"
Robert Nieuwenhuis, Albert Oliveras.
16th International Conference on Rewriting Techniques and Applications (RTA). April 2005, Nara (Japan).
[ Paper | BibTeX ]
"Abstract DPLL and Abstract DPLL Modulo Theories"
Robert Nieuwenhuis, Albert Oliveras, and Cesare Tinelli
11th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR). March 2005, Montevideo (Uruguay).
[ Paper | Slides | BibTeX ]
"DPLL(T): Fast Decision Procedures"
Harald Ganzinger, George Hagen, Robert Nieuwenhuis, Albert Oliveras, and Cesare Tinelli
16th International Conference on Computer Aided Verification (CAV), July 2004, Boston (USA).
[ Paper | Detailed experimental results | Slides | BibTeX ]
"Congruence Closure with Integer Offsets"
Robert Nieuwenhuis, Albert Oliveras.
10th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR). September 2003, Almaty (Kazakhstan).
[ Paper | Slides | BibTeX ]

Barcelogic:

All previous implementations were merged into our system Barcelogic for SMT. It won all four categories of the 2005 SMT-Competition in which it participated. In the 2006 SMT-Competition it came second in all categories in which it participated. You can visit the Barcelogic for SMT website.