Enric Rodríguez Carbonell

 I'm a researcher 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.  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).

3. 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]
 

4. 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).

5. 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]
 

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

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

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]
 

More stuff

1. Seminar on polynomial invariant inference at the University of Parma in January 2005, invited by Prof. Roberto Bagnara

1st part:    slides in [PDF]
2nd part:   slides in [PDF]

2. Talk on 08/06/2006 in Barcelona in [PS][PDF]

Some programs that need polynomial invariants in order to be verified  

cohendiv
divbin
hard
mannadiv
wensley

sqrt
dijkstra
z3sqrt
freire1
freire2

E-mail:

Phone:  (+34) 93 413 7861
Fax:      (+34) 93 413 7833

Some pictures taken in Dagstuhl