Albert Oliveras i Llunell

I'm Phd student at the Departament de Llenguatges i Sistemes Informàtics (LSI) of the Universitat Politècnica de Catalunya (UPC) in Barcelona, Spain.

Publications

• "Congruence Closure with Integer Offsets"
  Robert Nieuwenhuis, Albert Oliveras.
  10th International Conference for Programming, Artificial Intelligence and Reasoning (LPAR). September 2003, Almaty (Kazakhstan). 
  [ 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 | BibTeX]
   
• "Abstract DPLL and Abstract DPLL Modulo Theories"
  Robert Nieuwenhuis, Albert Oliveras, and Cesare Tinelli
  11th International Conference for Programming, Artificial Intelligence and Reasoning (LPAR). March 2004, Montevideo (Uruguay).
  [ Paper ]
   
• "Proof-producing Congruence Closure"
  Robert Nieuwenhuis, Albert Oliveras.
  16th International Conference on Rewriting Techniques and Applications (RTA). Abril 2004, Nara (Japan). 
  [ Paper ]
  

  
  

Sofware (available for Linux)

- DPLL(T) for EUF plus predecesor/succesor

• The first implementation of a DPLL(T) framework (described in the corresponding paper above) for deciding validity of formulas in EUF (with predecesor/successor) logic is already available. 
  [ Download] 
  
• Benchmarks for EUF with integer offsets are available in several formats. We thank the UCLID group for providing them.
  [ SVC | UCLID | DPLL(T) ]
  
• Translators between benchmarks formats.
  [ SVC --> DPLL(T) | SVC --> UCLID ]  

- DPLL(T) for Difference Logic

• This new instance of DPLL(T) decides the validity of formulas in Difference Logic over the integers.
  [ Download] 
  
• Benchmarks from Difference Logic are availabe in several formats.
  [ ICS | MathSAT | TSAT |  DPLL(T)]
• Comparison with other existing tools on the aforementioned benchmarks.
  [ Detailed experimental results] 
  

(Versions of the software in other platforms are available on demand.)

This page has been visited times since 22nd January, 2004.