Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456 Albert Oliveras i Llunell Home Page
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
]
"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)
]