Conference papers


2017

Cristina Borralleras, Marc Brockschmidt, Daniel Larraz, Albert Oliveras, Enric Rodr\'iguez-Carbonell and Albert Rubio.
Proving Termination through Conditional Termination [PDF].
In Tools and Algorithms for the Construction and Analysis of Systems - 23nd International Conference, TACAS 2017,
Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, April 2017, Uppsala (Sweden).
©Springer-Verlag.


2016

Lorenzo Candeago, Daniel Larraz, Albert Oliveras, Enric Rodríguez-Carbonell and Albert Rubio.
Speeding Up the Constraint-Based Method in Difference Logic [PDF].
In 19th International Conference on Theory and Applications of Satisfiability Testing (SAT'16), July 2016, Bordeaux (France).
©Springer-Verlag.


2015

Marc Brockschmidt, Daniel Larraz, Albert Oliveras, Enric Rodríguez-Carbonell and Albert Rubio.
Compositional Safety Verification with Max-SMT [PDF].
In 15th Formal Methods in Computer-Aided Design (FMCAD'15), September 2015, Austin (USA).
©ACM Press.


2014

Daniel Larraz, Kaustubh Nimkar, Albert Oliveras, Enric Rodríguez-Carbonell and Albert Rubio.
Proving Non-termination Using Max-SMT [PDF].
In 26th International Conference on Computer Aided Verification (CAV'14), July 2014, Viena (Austria).
©Springer-Verlag.


Daniel Larraz, Albert Oliveras, Enric Rodríguez-Carbonell and Albert Rubio.
Minimal-Model-Guided Approaches to Solving Polynomial Constraints and Extensions [PDF].
In 17th International Conference on Theory and Applications of Satisfiability Testing (SAT'14), July 2014, Viena (Austria).
©Springer-Verlag.


2013

Ignasi Abío, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell and Peter J. Stuckey.
To Encode or to Propagate? The Best Choice for Each Constraint in SAT [PDF].
In 19th International Conference on Constraint Programming (CP'13), September 2013, Uppsala (Sweden).
©Springer-Verlag.


Ignasi Abío, Robert Nieuwenhuis, Albert Oliveras and Enric Rodríguez-Carbonell.
A Parametric Approach for Smaller and Better Encodings of Cardinality Constraints [PDF].
In 19th International Conference on Constraint Programming (CP'13), September 2013, Uppsala (Sweden).
©Springer-Verlag.


Daniel Larraz, Albert Oliveras, Enric Rodríguez-Carbonell and Albert Rubio.
Proving Termination of Imperative Programs Using Max-SMT  [PDF].
In 13th Formal Methods in Computer-Aided Design (FMCAD'13), October 2013, Portland (USA).
©ACM Press.


Daniel Larraz, Enric Rodríguez-Carbonell and Albert Rubio.
SMT-Based Array Invariant Generation [PDF].
In 14th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'13), January 2013, Rome (Italy).
©Springer-Verlag.

Amalia Duch, Jordi Petit, Enric Rodríguez-Carbonell and Salvador Roura
Fun in CS2 [PDF].
In 5th International Conference on Computer Supported Education (CSEDU'13), May 2013, Aachen (Germany).


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.