Albert Oliveras i Llunell

Associate professor (professor agregat - profesor contratado doctor)
Technical University of Catalonia
CS Department, Building Omega, room 114
Member of the LOGPROG research group
Jordi Girona 1
E-08034 Barcelona
CATALONIA
E-mail: oliveras AT(NSPAM) cs.upc.edu
Phone: (34) 93 413 77 92
Fax: (34) 93 413 78 33

Education:

PhD. in Computer Science (defended July 2006), Department CS 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
Program Analysis

Publications (in reverse chronological order):

CONFERENCE PAPERS:

"Speeding Up the Constraint-Based Method in Difference Logic"
Lorenzo Candeago, Daniel Larraz, Albert Oliveras, Enric Rodríguez-Carbonell and Albert Rubio.
19th International Conference on Theory and Applications of Satisfiability Testing (SAT), July 2016, Bordeaux (France).
[ Paper ]
"Compositional Safety Verification with Max-SMT"
Marc Brockschmidt, Daniel Larraz, Albert Oliveras, Enric Rodríguez-Carbonell and Albert Rubio.
Formal Methods in Computer-Aided Design 2015 (FMCAD), September 2015, Austin, Texas (USA).
[ Paper ]
"Proving Non-termination Using Max-SMT"
Daniel Larraz, Kaustubh Nimkar, Albert Oliveras, Enric Rodríguez-Carbonell and Albert Rubio.
26th International Conference on Computer Aided Verification (CAV), July 2014, Vienna (Austria).
[ Paper ]
"Minimal-Model-Guided Approaches to Solving Polynomial Constraints and Extensions"
Daniel Larraz, Albert Oliveras, Enric Rodríguez-Carbonell and Albert Rubio.
17th International Conference on Theory and Applications of Satisfiability Testing (SAT), July 2014, Vienna (Austria).
[ Paper ]
"Proving Termination of Imperative Programs Using Max-SMT"
Daniel Larraz, Albert Oliveras, Enric Rodríguez-Carbonell and Albert Rubio.
Formal Methods in Computer-Aided Design 2013 (FMCAD), October 2013, Portland (USA).
[ Paper ]
"To Encode or To Progate? The Best Choice for Each Constraint in SAT"
Ignasi Abío, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell and Peter Stuckey.
19th International Conference on Principles and Practice of Constraint Programming (CP). September 2013, Uppsala (Sweden)
[ Paper ]
"A Parametric Approach for Smaller and Better Encodings of Cardinality Constraints"
Ignasi Abío, Robert Nieuwenhuis, Albert Oliveras and Enric Rodríguez-Carbonell.
19th International Conference on Principles and Practice of Constraint Programming (CP). September 2013, Uppsala (Sweden)
[ Paper ]
"BDDs for Pseudo-Boolean Constraints - Revisited"
Ignasi Abío, Robert Nieuwenhuis, Albert Oliveras and Enric Rodríguez-Carbonell.
14th International Conference on Theory and Applications of Satisfiability Testing (SAT). June 2011, Ann Arbor (USA)
[ Paper | BibTeX ]
"Semiring-Induced Propositional Logic: Definition and Basic Algorithms"
Javier Larrosa, Albert Oliveras and Enric Rodríguez-Carbonell.
16th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR). April 2010, Senegal (Dakar).
[ Paper | BibTeX ]
"Branch and Bound for Boolean Optimization and the Generation of Optimality Certificates"
Javier Larrosa, Robert Nieuwenhuis, Albert Oliveras and Enric Rodríguez-Carbonell.
12th International Conference on Theory and Applications of Satisfiability Testing (SAT). July 2009, Swansea (Wales).
[ Paper | BibTeX ]
"Cardinality Networks and their Applications"
Roberto Asín, Robert Nieuwenhuis, Albert Oliveras and Enric Rodríguez-Carbonell.
12th International Conference on Theory and Applications of Satisfiability Testing (SAT). July 2009, Swansea (Wales).
[ Paper | BibTeX ]
"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 | BibTeX ]
"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 ]

JOURNAL ARTICLES:

"A New Look at BDDs for Pseudo-Boolean Constraints"
Ignasi Abío, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, Valentin Mayer-Eichberger.
Journal of Artificial Intelligence Research (JAIR), 45: 443-480, 2012.
[ Paper | BibTeX ]
"6 Years of SMT-COMP"
Clark Barrett, Morgan Deters, Leonardo de Moura, Albert Oliveras and Aaron Stump.
Journal of Automated Reasoning (JAR), to appear.
[ Paper | BibTeX ]
"Cardinality Constraints: a Theoretical and Empirical Study"
Roberto Asín, Robert Nieuwenhuis, Albert Oliveras and Enric Rodríguez-Carbonell.
Constraints, 16(2):195-221.
[ Paper | BibTeX ]
"SAT Modulo Linear Arithmetic for Solving Polynomial Constraints"
Cristina Borralleras, Salvador Lucas, Albert Oliveras, Enric Rodríguez-Carbonell and Albert Rubio.
Journal of Automated Reasoning (JAR) 48(1): 107-131.
[ Paper | BibTeX ]
"A Framework for Certified Boolean Branch-and-Bound Optimization"
Javier Larrosa, Robert Nieuwenhuis, Albert Oliveras and Enric Rodríguez-Carbonell.
Journal of Automated Reasoning (JAR), 46(1):81-102.
[ Paper | BibTeX ]
"Practical algorithms for unsatisfiability proof and core generation in SAT solvers"
Roberto Asín, Robert Nieuwenhuis, Albert Oliveras and Enric Rodríguez-Carbonell.
AI Communications (AICOM), 23(2-3):145-157, 2010.
[ Paper | BibTeX ]
"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), 17(4):569-606, August 2008.
"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 ]

Professional activities (in reverse chronological order):

PC member for the 11th International Worshop on the Implementation of Logics (IWIL 2015). November 2015. Suva (Fiji).
PC member for the 18th International Conference on Theory and Applications of Satisfiability Testing (SAT'15). September 2015. Austin, Texas (USA).
Workshop Chair for the 18th International Conference on Theory and Applications of Satisfiability Testing (SAT'15). September 2015. Austin, Texas (USA).
PC member for the 25th International Conference on Automated Deduction (CADE-25). August 2015. Berlin (Germany).
PC member for the 29th International Conference on Artificial Intelligence (AAAI-15). January 2015. Austin, Texas (USA).
PC member for the XIV Jornadas sobre Programación y Lenguajes (PROLE 2014). September 2014. Cádiz (Spain).
PC member for the 21st European Conference on Artificial Intelligence (ECAI'14). August 2014. Prague (Czech Republic).
PC member for the 12th International Workshop on Satisfiability Modulo Theories (SMT'14). July 2014. Vienna (Austria).
PC member for the 17th International Conference on Theory and Applications of Satisfiability Testing (SAT'14). July 2014. Vienna (Austria).
PC member for the 19th International Conference on Logic for Programming, Artificial Intelligence and Resoning (LPAR 2013). December 2013. Stellenbosch (South Africa).
PC member for the XIII Jornadas sobre Programación y Lenguajes (PROLE 2013). September 2013. Madrid (Spain).
PC member for the 16th International Conference on Theory and Applications of Satisfiability Testing (SAT 2013). June 2013. Helsinki (Finland).
PC member for the XII Jornadas sobre Programación y Lenguajes (PROLE 2012). September 2012. Almería (Spain).
PC member for the 4th Workshop on Logic and Search (Lash'12). August 2012. Montpellier (France).
PC member for the 24th International Conference on Computer-Aided Verification (CAV 2012). July 2012. Berkeley, California (USA).
PC member for the Workshop on Pragmatics of SAT (PoS'12). June 2012. Trento (Italy).
PC member for the 3rd Workshop on Practical Aspects of Automated Reasoning (PAAR'12). June 2012. Manchester (UK).
PC member for the 6th International Joint Conference on Automated Reasoning (IJCAR 2012). June 2012. Mancester (United Kingdom).
PC member for the 9th International Worshop on the Implementation of Logics (IWIL 2012). March 2012. Mérida (Venezuela).
PC member for the 18th International Conference on Logic for Programming, Artificial Intelligence and Resoning (LPAR 2012). March 2012. Mérida (Venezuela).
PC member for the XI Jornadas sobre Programación y Lenguajes (PROLE 2011). September 2011. La Coruña (Spain).
PC member for the Workshop on Logics for Component Configuration (LoCoCo 2011). June 2011. Perugia (Italy).
PC member for the 14th International Conference on Theory and Applications of Satisfiability Testing (SAT 2011). June 2011. Ann Arbor (USA).
PC member for the 23rd International Conference on Automated Deduction (CADE-23). August 2011. Wroclaw (Poland).
PC member for the 8th International Workshop on the Implementation of Logics (IWIL'10). October 2010. Yogyakarta (Indonesia).
Co-organizer of the 6th International Satisfiability Modulo Theories Competition (SMT-COMP 2010). July 2010. Edinburgh (Scotland). August 2009. Montreal (Canada).
PC member for the Workshop on Logics for Component Configuration (LoCoCo'10). July 2010. Edinburgh (Scotland).
PC member for the 2nd Workshop on Practical Aspects of Automated Reasoning (PAAR'10). July 2010. Edinburgh (Scotland).
PC member for the 13th International Conference on Theory and Applications of Satisfiability Testing (SAT 2010). July 2010. Edinburgh (Scotland).
PC member for the 12th International Conference on Theory and Applications of Satisfiability Testing (SAT 2009). July 2009. Swansea (United Kingdom).
PC member for the 7th International Workshop on Frontiers of Combining Systems (FroCoS 2009). September 2009. Trento (Italy).
Co-organizer of the 5th International Satisfiability Modulo Theories Competition (SMT-COMP 2009). August 2009. Montreal (Canada).
PC member for the 22nd International Conference on Automated Deduction (CADE-22), August 2009. Montreal (Canada).
PC member for the 7th International Workshop on the Implementation of Logics (IWIL'08) , November 2008. Doha (Qatar).
PC member for the 1st Workshop on Practical Aspects of Automated Reasoning (PAAR'08). August 2008. Sidney (Australia).
Co-organizer of the 4th International Satisfiability Modulo Theories Competition (SMT-COMP 2008). July 2008. Princeton (USA).
PC member for the 6th International Workshop on Satisfiability Modulo Theories (SMT'08). July 2008. Princeton (USA).
Co-organizer of the 3rd International Satisfiability Modulo Theories Competition (SMT-COMP 2007). July 3-7, 2007. Berlin (Germany).
PC member for the 6th International Workshop on Frontiers of Combining Systems (FroCoS 2007). September 2007. Liverpool (United Kingdom).
PC member for the 21st International Conference on Automated Deduction (CADE-21). July 17-20, 2007. Bremen (Germany).
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 6th International Workshop on the Implementation of Logics (IWIL'06), November 12th, 2006. Phnom Penh (Cambodia).

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.