Conference papers


2011

Ignasi Abío, Robert Nieuwenhuis, Albert Oliveras and Enric Rodríguez-Carbonell.
BDDs for Pseudo-Boolean Constraints - Revisited [PDF].
In 14th International Conference on Theory and Applications of Satisfiability Testing (SAT'11), June 2011, Ann Arbor (USA).
©Springer-Verlag.


2010

Javier Larrosa, Albert Oliveras and Enric Rodríguez-Carbonell.
Semiring-Induced Propositional Logic: Definition and Basic Algorithms [PDF].
In 16th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-16), April 2010, Dakar (Senegal).


2009

Cristina Borralleras, Salvador Lucas, Rafael Navarro-Marset, Enric Rodríguez-Carbonell and Albert Rubio.
Solving non-linear polynomial arithmetic via SAT modulo linear arithmetic [PDF].
In 22nd International Conference on Automated Deduction  (CADE-22), August 2009, Montreal (Canada).
©Springer-Verlag.

Javier Larrosa, Robert Nieuwenhuis, Albert Oliveras and Enric Rodríguez-Carbonell.
Branch and Bound for Boolean Optimization and the Generation of Optimality Certificates [PDF].
In 12th International Conference on Theory and Applications of Satisfiability Testing (SAT'09), June 2009, Swansea (UK).
©Springer-Verlag.

Roberto Asín, Robert Nieuwenhuis, Albert Oliveras and Enric Rodríguez-Carbonell.
Cardinality Networks and their Applications [PDF].
In 12th International Conference on Theory and Applications of Satisfiability Testing (SAT'09), June 2009, Swansea (UK).
©Springer-Verlag.


2008

Marc Bezem, Robert Nieuwenhuis and Enric Rodríguez-Carbonell.
The Max-Atom Problem and its Relevance [PDF].
In 15th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR'08), November 2008, Doha (Qatar).
©Springer-Verlag.

Roberto Asín, Robert Nieuwenhuis, Albert Oliveras and Enric Rodríguez-Carbonell.
Efficient Generation of Unsatisfiability Proofs and Cores in SAT [PDF].
In 15th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR'08), November 2008, Doha (Qatar).
©Springer-Verlag.

Miquel Bofill, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell and Albert Rubio.
A Write-Based Solver for SAT Modulo the Theory of Arrays [PDF].
In 8th Formal Methods in Computer-Aided Design (FMCAD'08), November 2008, Portland (USA).
©ACM Press.

Miquel Bofill, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell and Albert Rubio.
The Barcelogic SMT Solver [PDF][BibTex].
In 20th International Conference on Computer Aided Verification (CAV'08), July 2008, Princeton (USA).
©Springer-Verlag.


Germain Faure, Robert Nieuwenhuis, Albert Oliveras and Enric Rodríguez-Carbonell.
SAT Modulo the Theory of Linear Arithmetic: Exact, Inexact and Commercial Solvers [PDF][BibTex].
In 11th International Conference on Theory and Applications of Satisfiability Testing (SAT'08), May 2008, Guangzhou (China).
Slides in [PDF].
©Springer-Verlag.


2007

Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell and Albert Rubio.
Challenges in Satisfiability Modulo Theories (Invited Paper) [PS][PDF][BibTex].
In 18th International Conference on Rewriting Techniques and Applications (RTA'07), June 2007, Paris (France).
©Springer-Verlag.


   
2005

Roberto Bagnara, Enric Rodríguez-Carbonell and Enea Zaffanella. 
Generation of Basic Semi-algebraic Invariants Using Convex Polyhedra [PS][PDF][BibTex].
In 12th International Symposium on Static Analysis (SAS'05), September 2005, London (UK).
Slides in [PS],[PDF].
©Springer-Verlag.


Robert Clarisó, Enric Rodríguez-Carbonell and Jordi Cortadella.
Derivation of Non-structural Invariants of Petri Nets Using Abstract Interpretation [PDF][BibTex].
In 26th International Conference On Application and Theory of Petri Nets and Other Models of Concurrency (ICATPN'05), June 2005, Miami (USA).
©Springer-Verlag.


Enric Rodríguez-Carbonell and Ashish Tiwari. 
Generating Polynomial Invariants for Hybrid Systems [PS][PDF][BibTex].
In 8th International Workshop on Hybrid Systems : Computation and Control (HSCC'05),  March 2005, Zurich (Switzerland).
Slides in [PS],[PDF].
©Springer-Verlag.


Enric Rodríguez-Carbonell and Jordi Cortadella.
Inference of Numerical Relations from Digital Circuits [PS].
Presented in 1st International Workshop on Numerical & Symbolic Abstract Domains 2005 (NSAD'05), January 2005, Paris (France).
Slides in [PS],[PDF].



2004

Enric Rodríguez-Carbonell and Deepak Kapur. 
Program Verification Using Automatic Generation of Invariants [PS][PDF][BibTex].
In 1st International Colloquium on Theoretical Aspects of Computing 2004 (ICTAC'04), September 2004, Guiyang (China).
Slides in [PS], [PDF].
©Springer-Verlag.


Enric Rodríguez-Carbonell and Deepak Kapur. 
An Abstract Interpretation Approach for Automatic Generation of Polynomial Invariants [PS][PDF][BibTex].
In 11th Static Analysis Symposium 2004 (SAS'04), August 2004, Verona (Italy).
Slides in [PS],[PDF].
©Springer-Verlag.


Enric Rodríguez-Carbonell and Deepak Kapur. 
Automatic Generation of Polynomial Loop Invariants: Algebraic Foundations [PS][PDF][BibTex].
In International Symposium on Symbolic and Algebraic Computation 2004 (ISSAC'04), July 2004, Santander (Spain).
Slides in [PS], [PDF].
© ACM Press. 
This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in ISSAC'04.