Enric Rodríguez Carbonell

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

I'm currently working on program verification and invariant inference.  Recently I've also become interested in the verification of arithmetic circuits (see papers below).

This website contains postscript/pdf files of articles that may be covered by copyright. You may browse the articles at your convenience (in the same spirit as you may read a journal or a proceeding article in a public library). Retrieving, copying, distributing these files may violate the copyright protection law. We recommend that the user abides international law in accessing this directory.
 
 

Papers (short versions)
 

1. Enric Rodríguez-Carbonell and Deepak Kapur.  Automatic Generation of Polynomial Loop Invariants: Algebraic Foundations [PS][PDF][BibTex], © ACM(2004). In International Symposium on Symbolic and Algebraic Computation 2004 (ISSAC'04), July 2004, Santander (Spain). 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.

Slides in [PS], [PDF]
 

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

Slides in [PS], [PDF]
 

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

Slides in [PS],[PDF]
 

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

Slides in [PS],[PDF]
 

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

Slides in [PS],[PDF]
 
 

Reports (extended versions of the papers)
 

1. Enric Rodríguez-Carbonell and Deepak Kapur.  Automatic Generation of Polynomial Loop Invariants: Algebraic Foundations [PS][PDF]
 

2. Enric Rodríguez-Carbonell and Deepak Kapur.  Program Verification Using Automatic Generation of Invariants [PS][PDF]
 

3. Enric Rodríguez-Carbonell and Deepak Kapur.  An Abstract Interpretation Approach for Automatic Generation of Polynomial Invariants [PS][PDF]
 
 

Some programs that need polynomial invariants in order to be verified
 

cohendiv
dershowitz
euclidex1
euclidex3
fermat
fermatorig
hard
lcm
prodbin
readers_writers
z3sqrt
freire1
freire2
cohencu
divbin
dijkstra
fermat2
wensley2
euclidex2
lcm2
factor
prod4br
sqrt

E-mail:

Phone:  (+34) 93 413 7861
Fax:      (+34) 93 401 7014