Roberto, Margherita and Beatrice

Home

Personal Info

Papers

Teaching

Links

Curriculum Vitae et Studiorum of Roberto Bagnara

CURRICULUM VITAE ET STUDIORUM

CURRICULUM VITAE ET STUDIORUM

Roberto Bagnara





Contents

Curriculum vitae et studiorum of Roberto Bagnara

1  Personal Data

Surname:Bagnara
First name:Roberto
Date of birth:December 7, 1963
Town of birth:Faenza (RA), Italy
Nationality:Italian
Passport:F924127 delivered by Questura di Lucca (Italy),
 date of expiry: July 5, 2016
Profession:Full professor
Personal status:Married, two children
Languages known:Italian, English, French and Spanish

1.1  Addresses

Work:Department of Mathematics and Computer Science
 University of di Parma
 Parco Area delle Scienze 53/A
 I-43124 Parma
 Italy
 Tel: +39 0521 906917 — Fax: +39 0521 906950
  
Home:Via di Belvedere 1
 57028 Suvereto (LI)
 Tel: +39 0565 828310
  
Mobile:+39 339 8593517
Email:bagnara@cs.unipr.it

1.2  Current professional position

Full professor of Computer Science (Informatica) at the Department of Mathematics and Computer Science of the University of Parma, Italy.

1.3  Degrees

  • Non-graduate Engineer for Telecommunications, Industrial Technical Institute of Cesena (FO), Italy, 1982.
  • M.Sc. in Computer Science (Laurea in Scienze dell’Informazione) with Full Marks and Honors, University of Pisa, Italy, 1992.
  • Ph.D. in Computer Science (Dottorato di ricerca in Informatica), Department of the Computer Science, University of Pisa, Italy, 1997.

1.4  Foreign languages spoken and written

English (advanced), French (advanced) and Spanish (intermediate).

2  Curriculum vitae et studiorum

1978–1982:
Non-graduate Engineer for Telecommunications, Industrial Technical Institute of Cesena (FO), Italy.
1983–1984:
Italian military service.
1984–1987:
Technical Assistant at the Physics Department (Medical Physics Group) of the University of Bologna, Italy.
1988–1989:
Technical Student Fellow (1988) and Consultant (1989) at CERN, Data Handling Division, Online Computing Group, Readout Architecture Section, Geneva, Switzerland.
1989–1992:
M.Sc. in Computer Science (Laurea in Scienze dell’Informazione) with Full Marks and Honors, University of Pisa, Italy.
1992–1996:
Research activity as PhD student at the Computer Science Department of the University of Pisa, Italy. Doctorate degree officially awarded on September 8, 1997.
1997:
Research fellow at the School of Computer Studies of the University of Leeds, United Kingdom.
1997–2001
Research and teaching activity as Assistant Professor (Ricercatore) at the Department of Mathematics of the University of Parma, from November 1st, 1997 to December 15th, 2001.
2001–2010:
From December 16th, 2001, to October 31st, 2010, research and teaching activity as Associate Professor at the Department of Mathematics of the University of Parma, Italy. Among other things, he contributed to the creation of the Degree in Computer Science (Informatica) of the University of Parma.
2011:
Foundation of the university spin-off BUGSENG srl.
Presently:
Since November 1st, 2010, research and teaching activity as Full Professor at the Department of Mathematics and Computer Science of the University of Parma, Italy. Since the foundation, he is the President and CEO of BUGSENG srl.

3  Teaching Activities

3.1  Courses Taught

All the activities listed in this section refer to courses of studies of the University of Parma.

  1. “Informatica” (Computer Science), degree in “Biotechnologies”, academic years 1999-2000 and 2000-2001.
  2. “Laboratorio di informatica” (Laboratory of Computer Science), degree in “Mathematics”, academic year 2000-2001.
  3. “Programmazione (metodi avanzati)” (Advanced Programming Techniques), degree in “Mathematics”, academic years 2000-2001 and 2002-2003.
  4. “Programmazione 3” (3rd course on Programming), degrees in “Mathematics” and “Mathematics and Computer Science”, academic year 2002-2003.
  5. “Scrittura matematica e informatica” (Writing for Mathematics and Computer Science), degrees in “Mathematics” and “Mathematics and Computer Science”, academic year 2002-2003.
  6. “Programmazione I” (1st course on Programming), degrees in “Mathematics”, “Mathematics and Computer Science” e “Mathematics for Technology and Finance”, academic year 2001-2002.
  7. “Fondamenti dell’informatica” (Foundations of Computer Science), degrees in “Mathematics” e “Mathematics and Computer Science”, academic years 2002-2003, 2003-2004, 2004-2005, 2006-2007, 2007-2008, 2008-2009, 2009-2010, 2010-2011, 2011-2012 and 2012-2013.
  8. “Fondamenti dell’informatica” (Foundations of Computer Science), degree in “Computer Science”, academic years 2002-2003, 2003-2004, 2005-2006, 2006-2007, 2007-2008, 2008-2009, 2009-2010, 2010-2011, 2011-2012 and 2012-2013.
  9. “Scrittura matematica e informatica” (Writing for Mathematics and Computer Science), degree in “Computer Science”, academic years 2003-2004, 2004-2005 and 2005-2006.
  10. “Linguaggi di programmazione” (Programming Languages), degree in “Computer Science”, academic year 2006-2007, 2007-2008, 2008-2009, 2009-2010 and 2010-2011.
  11. “Analisi e verifica del software” (Analysis and Verification of Software), degree in “Computer Science”, academic years 2003-2004, 2004-2005, 2005-2006, 2006-2007, 2007-2008, 2008-2009.
  12. “Computer Aided Verification of Complex Systems: An Introduction”, Ph.D. School (Dottorato di ricerca) in “Matematica e Statistica per le Scienze Computazionali” (Mathematics and Statistics for the Computational Sciences), Department of Mathematics, University of Milan, academic year 2006-2007.
  13. “Algorithmique” (Algorithmics), Licence de mathématiques, Université de la Réunion, academic year 2006-2007.
  14. “Laboratorio di informatica” (Laboratory of Computer Science), Degree in “Environmental Sciences”, University of Siena, Follonica (GR), academic year 2007-2008.
  15. “Réécriture et Sémantique” (Rewriting and Semantics), Master Sciences et Technologies, Mention Informatique et Mathématiques, Spécialité STIC, Université de la Réunion, academic year 2009-2010.
  16. “Semantica dei linguaggi di programmazione” (Semantics of Programming Languages), degree in “Computer Science”, academic years 2010-2011, 2011-2012 e 2012-2013.

3.2  Teaching Collaborations

  1. Lectures (8 hours) on The Compilation of Prolog and the Warren Abstract Machine in the course on “Linguaggi speciali di programmazione” (Special-Purpose Programming Languages) taught by Prof. Giorgio Levi, degree in “Computer Science” of the Universityof Pisa, academic years 1990-1991, 1991-1992, 1992-1993 and 1993-1994.
  2. Exercise classes for the course on “Linguaggi formali e compilatori” (Formal Languages and Compilers) taught by Prof. Pierpaolo Degano, degree in “Computer Science” of the Universityof Pisa, academic year 1995-1996,
  3. Theory and exercise classes for the course on “Teoria ed applicazioni delle macchine calcolatrici” (Theory and Application of Computing Machines) taught by Prof. Gianfranco Rossi, degree in “Environmental Sciences” of the University of Parma, academic years 1997-1998, 1998-1999, 1999-2000 and 2000-2001.
  4. Theory and exercise classes for the course on “Fondamenti dell’informatica” (Foundations of Computer Science) taught by Prof. Grazia Lotti, degree in “Mathematics” of the University of Parma, academic years 1998-1999 and 1999-2000.
  5. Classes and support to student projects for the course on “Metodologie di programmazione” (Programming Methodologies) taught by Dr. Enea Zaffanella, degree in “Conputer Science” of the University of Parma, academic years 2003-2004 and 2004-2005.

3.3  Activity as Advisor and Co-Advisor for M.Sc. (Laurea) Theses

  1. Motta, M. Un’implementazione efficiente ed innovativa del dominio Pos per l’analisi statica di programmi logici (An Efficient and Innovative Implementation of the Pos Domain for the Static Analysis of Logic Programs). Laurea thesis in “Computer Science”. Advisor: G. Levi; co-advisor: R. Bagnara. University of Pisa. Academic year 1994-1995.
  2. Scudellari, M. C. Analisi bottom-up di programmi logici con vincoli basata su trasformazioni Magic-Set (Bottom-Up Analysis of Constraint Logic Programs Based on Magic-Set Transformations). Laurea thesis in “Computer Science”. Advisor: G. Levi; co-advisor: R. Bagnara. University of Pisa. Academic year 1994-1995.
  3. Castellacci, B. Implementazione di un’analisi di tipi per programmi logici basata su grammatiche regolari (Implementation of a Type Analysis for Logic Programs Based on Regular Grammars). Laurea thesis in “Computer Science”. Advisor: G. Levi; co-advisor R. Bagnara. University of Pisa. Academic year 1995-1996.
  4. Stazzone, A. Annotazione e trasformazione di programmi logici con vincoli (Annotation and Transformation of Constraint Logic Programs). Laurea thesis in “Mathematics”. University of Parma. Advisor: R. Bagnara; co-advisor: E. Zaffanella. Academic year 1999-2000.
  5. Ricci, E. Rappresentazione e manipolazione di poliedri convessi per l’analisi e la verifica di programmi (Representation and Manipulation of Convex Polyhedra for Program Analysis and Verification). Laurea thesis in “Mathematics”. University of Parma. Advisor: R. Bagnara; co-advisors: C. Medori ed E. Zaffanella. Academic year 2001-2002.
  6. Zolo, T. Risoluzione automatica di relazioni di ricorrenza (Automatic Solution of Recurrence Relations). Laurea thesis in “Mathematics”. University of Parma. Advisor: R. Bagnara; co-advisors: A. Zaccagnini ed E. Zaffanella. Academic year 2001-2002.
  7. Pescetti, A. L’algoritmo di Zeilberger per la risoluzione automatica di ricorrenze (Zeilberger’s Algorithm for the Automatic Solution of Recurrences). Laurea thesis in “Mathematics”. University of Parma. Advisor: R. Bagnara; co-advisor: A. Zaccagnini. Academic year 2004-2005.
  8. Cimino, A. Un’implementazione incrementale e su aritmetica esatta del simplesso primale (An Incremental Implementation of Primal Simplex with Exact Arithmetic). Laurea thesis in “Computer Science”. University of Parma. Advisor: E. Zaffanella; co-advisor: R. Bagnara. Academic year 2004-2005.
  9. Vincenzi, A. Interpretazione astratta di operatori per la manipolazione di bit in linguaggi imperativi (Abstract Interpretation of Bitwise Operators in Imperative Languages). Laurea thesis in “Computer Science”. University of Parma. Advisor: R. Bagnara; co-advisor: E. Zaffanella. Academic year 2005-2005.
  10. Quartieri, B. Implementazione efficiente di domini astratti numerici debolmente relazionali (Efficient Implementation of Weakly Relational Abstract Domains). Laurea thesis in “Mathematics”. University of Parma. Advisor: R. Bagnara; co-advisor: E. Zaffanella. Academic year 2005-2006.
  11. Franchi, E. A contribution to the issue of string cleanness: a design of an automatic program transformation. Laurea thesis in “Mathematics and Computer Science”, University of Parma. Advisor: R. Bagnara; co-advisor: E. Zaffanella; Academic year 2006-2007.
  12. Soffia, S. Definizione ed implementazione di una analisi di points-to per linguaggi C-like (Definition and Implementation of a Points-To Analysis for C-Like Languages). Laurea thesis in “Computer Science”, University of Parma. Advisor: R. Bagnara; co-advisor: E. Zaffanella; Academic year 2007-2008.
  13. Bossi, F. CORAL: a modern C++library for the manipulation of Boolean functions. Laurea thesis in “Computer Science”, University of Parma. Advisor: R. Bagnara. Academic year 2007-2008.
  14. Bolzoni, P. Automatic checking of coding rules. Laurea thesis in “Computer Science”, University of Parma. Advisor: R. Bagnara; co-advisor: E. Zaffanella; Academic year 2008-2009.
  15. Poletti, M. Progettazione ed implementazione di matrici sparse basate su strutture dati cache-oblivious. (Design and Implementation of Sparse Matrices Based on Cache-Oblivious Data Structures). Laurea thesis in “Computer Science”, University of Parma. Advisor: E. Zaffanella; co-advisor: R. Bagnara Academic year 2009-2010.
  16. Boscolo, A. M. Un configuratore web-based per un framework di verifica software. (A Web-Based Configurator for a Software Verification Framework). Laurea thesis in “Computer Science”, University of Parma. Advisor: R. Bagnara. Academic year 2010-2011.

3.4  Ph.D. Schools

  1. Since 2000, teacher of the Ph.D. School (Dottorato di ricerca) in “Matematica e Statistica per le Scienze Computazionali” (Mathematics and Statistics for the Computational Sciences), Department of Mathematics, University of Milan.

3.5  PhD Committees

  1. Gómez-Zamalloa Gil, M. Transformación y Análisis de Código de Bytes Orientado a Objetos (Transformation and Analysis of Object-Oriented Bytecode). Departamento de Sistemas Informáticos y Computación, Universidad Complutense de Madrid. October 2009.
  2. Visentini, E. Exploiting Loop Transformations for the Protection of Software. Dipartimento di Informatica, Università degli Studi di Verona. April 2010.

3.6  Other Teaching Activities

  1. Lectures on fundamentals of Computer Science for the specialization course for high-school teachers of Mathematics organized by the Faculty of Sciences of the University of Parma, academic years 1997-1998 and 1998-1999.
  2. A computer and computing primer for the teachers of the maternal and primary schools of Suvereto, Italy, 1999.

4  Research Activities

4.1  Research Interests

  • Verification of critical software
  • Formal methods for the analysis and verification of programs
  • Semantics of programming languages
  • Abstract interpretation
  • Advanced compilation techniques
  • Logic programming and constraint logic programming
  • Computer algebra

4.2  Research Periods and Activities Outside Italy

  1. Technical Student Fellow at CERN (European Organization for Nuclear Research), Geneva, Switzerland, January–September 1988.
  2. Consultant at CERN (European Organization for Nuclear Research), Geneva, Switzerland, July–August 1989.
  3. Visiting researcher at the Department of Computer Science of the Monash University, Melbourne, Australia, for a joint research with the group of Prof. Kim Marriott, January–February 1995.
  4. Research fellow at the School of Computer Studies of the University of Leeds, UK, January–October 1997.
  5. Starting from 1998, numerous visits (at least one week per year) the School of Computing of the University of Leeds for joint research periods with Dr Patricia M. Hill.
  6. Withing the framework of exchanges between Italy and Spain, spent one week at the Facultad de Informática, Universidad Politécnica de Madrid for joint research with the group of Prof. Manuel Hermenegildo, January–February 2001.
  7. In the framework of the bilateral project on “Advanced Development Environments for Logic Programs” (Azioni Integrate Italia-Spagna 2001, code IT229), three one-week visits at the Facultad de Informática, Universidad Politécnica de Madrid for joint research with the group of Prof. Manuel Hermenegildo, November 2001, September 2002 and May 2003.
  8. Visiting scientist at the Laboratoire d’Informatique of the École Polytechnique (LIX, Paris), June–July 2008.
  9. Professeur invité at the Département de Mathématiques et Informatique of the Université de La Réunion, St Denis (Indian Ocean, France), May 2002, June 2005, May 2006, May 2007, and March 2010.

4.3  Keynote Speeches

  1. Keynote speaker at the “2011 Meeting on Rich-Model Toolkit: Infrastructure for Reliable Computer Systems” and the “2011 Symposium on Software Technologies Concertation on Formal Methods for Components and Objects” (FMCO 2011), Natural Science Museum of Turin, Turin, Italy, October 3, 2011. Titolo: The Automatic Synthesis of (Linear) Ranking Functions for Termination Analysis.
  2. Keynote speaker at the “13th International Conference on Quality Software” (QSIC 2013), Nanjing, China, July 29–30, 2013. Title: Quality Verification Tools for Quality Software.

4.4  Seminars

  1. “Introduction to the Warren Abstract Machine”, Dipartimento di Informatica, University of Pisa, March 1991.
  2. “Data-Flow Analysis for Constraint Logic-Based Languages”, School of Computer Studies, University of Leeds, March 1997.
  3. “Analisis eficiente de informacion estructural para lenguajes de programacion logica y de restricciones”, Departamento de Inteligencia Artificial, Universidad Politécnica de Madrid, January 2001.
  4. “Widening Sharing”, Departamento de Inteligencia Artificial, Universidad Politécnica de Madrid, January 2001.
  5. “The Parma Polyhedra Library”, Institut de Recherche en Mathématiques et Informatique Appliquées, Université de La Réunion, May 2002.
  6. “Symbolic Computation Support for Complexity Analysis and the PURRS Project”, Facultad de Informática, Universidad Politécnica de Madrid, May 2003.
  7. “Convex Polyhedra for the Analysis and Verification of Hardware and Software Systems: the ‘Parma Polyhedra Library”, Dipartimento di Matematica, University of Parma, December 2003.
  8. “Representation and Manipulation of Not Necessarily Closed Convex Polyhedra”, Dipartimento di Matematica, University of Parma, February 2004.
  9. “Abstract Interpretation and the Parma Polyhedra Library: from Theory to Practice and Vice Versa”, Dipartimento di Informatica, Sistemi e Produzione, University of Roma “Tor Vergata”, November 2004.
  10. “Analysis and Verification of Software Systems via Abstract Interpretation: An Informal Introduction”, Dipartimento di Ingegneria dell’Informazione, University of Siena, January 2006.
  11. “Applications of Polyhedral Computations to the Analysis and Verification of Hardware and Software Systems”, Polyhedral Computation Worskhop, Centre de recherches mathématiques, University of Montréal, Montréal (Québec), Canada, October 2006 (invited talk).
  12. “The Parma Polyhedra Library: A Library of Numerical Abstractions for Analysis and Verification”, Department of Informatics and Mathematical Modelling, Technical University of Denmark (DTU), Lyngby, Denmark, June 2007.
  13. “Numerical Abstract Domains”, Department of Communication, Business and Information Technologies (CBIT), Roskilde University, Roskilde, Denmark, June 2007.
  14. “On the Design of Generic Static Analyzers for Modern Imperative Languages”, Copenhagen Programming Language Seminar (COPLAS), Department of Computer Science (DIKU), University of Copenhagen, Copenhagen, Denmark, June 2007.
  15. “On the Design of Generic Static Analyzers for Modern Imperative Languages”, Facultad de Informática, Universidad Politécnica de Madrid, Madrid, Spain, September 2007.
  16. “Ranking Functions for Automatic Termination Analysis”, Department of Computer Science, University of Bologna, Italy December 2007.
  17. “On the Design of Generic Static Analyzers for Imperative Languages”, Department of Computer Science, University of Pisa, Italy, March 2008.
  18. “Computer Aided Verification of Complex Systems: An Introduction”, Department of Mathematics, University of Milan, Italy, March 2008.
  19. “Numerical Abstract Domains and the Parma Polyhedra Library”, Department of Computer Science, University of Verona, Italy, January 2010.
  20. “Syntactic and Semantic Analysis of Safety-Critical Software”, Safety Critical Systems Club workshop on Using the MISRA Guidelines to Support Safety-Related Systems Development, Ambassadors Bloomsbury, London, UK, November 2010.
  21. “Formal Methods: A Gentle Introduction”, Atego/HighRely workshop on DO-178 & DO-254 Avionics Certification, Milan, Italy May 2012.
  22. “Une introduction informelle aux méthodes formelles”, IRILL, Paris, November 2012.
  23. “The Automatic Synthesis of (Linear) Ranking Functions for Termination Analysis”, Université Paris Diderot, Paris, November 2012.

4.5  Program Committees

  1. Program Committee member for the “2000 Joint Conference on Declarative Programming”, La Habana, Cuba, December 4–7, 2000.
  2. Program Committee member for the 13th “Workshop on Logic Programming Environments”, Mumbai, India, December 8, 2003.
  3. Member of the comité de lecture of the 13th edition of the “Journées Francophones de Programmation en Logique et de programmation par Contraintes” (JFPLC 2004), Angers, France, June 21–23, 2004,
  4. Program Committee member for the “International Symposium on Logic-based Program Synthesis and Transformation” (LOPSTR’05), London, UK, September 7–9, 2005.
  5. Program Committee member for the 21st “International Conference on Logic Programming” (ICLP’05), Barcelona, Spain, October 2–5, 2005.
  6. Program Committee member for the 16th “International Symposium on Logic-based Program Synthesis and Transformation” (LOPSTR 2006), S. Servolo, Venice, Italy, July 12–14, 2006.
  7. Scientific Committee member of the Second Workshop on Open Source, Free Software and Open Formats in Archaeological Research Processes, Genova, Italy, May 11, 2007.
  8. Scientific Committee member of the Third Workshop on Open Source, Free Software and Open Formats in Archaeological Research Processes, Padua, Italy, May 8–9, 2008.
  9. Program Committee member for the Technical Track on Software Verification of the 23rd “Annual ACM Symposium on Applied Computing” (SAC 2008), Fortaleza, Ceará, Brazil, March 16–20, 2008.
  10. Program Committee member for the 9th “International Conference on Verification, Model Checking and Abstract Interpretation” (VMCAI 2008), San Francisco, USA, January 7–9, 2008.
  11. Program Committee member for the 15th “International Static Analysis Symposium” (SAS 2008), Valencia, Spain, July 16–18, 2008.
  12. Program Committee member for the “Colloquium on Implementation of Constraint and Logic Programming Systems” (CICLOPS 2008), Udine, December 12–13, 2008.
  13. Program Committee member for the 19th “International Symposium on Logic-based Program Synthesis and Transformation” (LOPSTR 2009), Coimbra, Portugal, September 9–11, 2009.
  14. Scientific Committee member of ArcheoFOSS 2010, Foggia, Museo Civico, May 6-7, 2010.
  15. Program Committee member for the “15th Portuguese Conference on Artificial Intelligence, Thematic Track: COLA - COmputational Logic with Applications” (EPIA 2011), Universidade de Lisboa, Portugal, October 10–13, 2011.
  16. Program Committee member for the “13th International Conference on Quality Software” (QSIC 2013), Nanjing, China, July 29–30, 2013.
  17. Program Committee member for the “29th International Conference on Logic Programming” (ICLP 2013), Istambul, Turkey, August 24–29, 2013.
  18. Program Committee member for the “22nd EACSL Annual Conference on Computer Science Logic” (CSL 2013), Turin, Italy, September 2–5, 2013.
  19. Program Committee member for the Software Engineering in Practice (SEIP) track of the “36th International Conference on Software Engineering” (ICSE 2014), Hyderabad, India, May 31 – June 7, 2014.

4.6  Standardization

  1. Represents Italy in working group ISO/IEC JTC 1/SC 22/WG 14 “The Programming Language C”.

4.7  Organization of Schools, Conferences, Workshops and Seminars

  1. Workshop Chair for the “Joint International Symposia SAS’98 and PLILP-ALP’98”, Pisa, Italy, September 14–18, 1998.
  2. Organizer, with Patricia M. Hill of the University of Leeds of the “Second International Summer School on Computational Logic”, Maratea, Italy, August 25–30, 2002 (http://www.cs.unipr.it/ISCL02/).
  3. Organizer of a cycle of seminars on “Convex Polyhedra for the Analysis and Verification of Hardware and Software Systems”, Dipartimento di Matematica, University of Parma, November 2003 – February 2004 (http://bugseng.com/products/pplseminars_2003_2004).
  4. Member of the organizing committee of CILC’04 – Convegno Italiano di Logica Computazionale, 19th annual meeting of the “Associazione Italiana Gruppo Ricercatori e Utenti di Logic Programming” (GULP), Dipartimento di Matematica, University of Parma, June 16–17, 2004 (http://www.cs.unipr.it/CILC04/).
  5. Scientific Committee member and organizer (with Giancarlo Macchi) of the First Workshop on Open Source, Free Software and Open Formats in Archaeological Research Processes, Grosseto, Italy, May 8, 2006.
  6. Scientific Committee member and organizer (with Giancarlo Macchi) of the I-QMDAA Summer School on Quantitative Methods and Data Analysis in Archaeology, Villa Lanzi, Campiglia Marittima, Italy, September 10–17, 2006.
  7. Workshop coordinator (with Nicos Angelopoulos) of the “12th International Colloquium on Implementation of Constraint and LOgic Programming Systems” (CICLOPS 2012), Budapest, Hungary, September 4, 2012.

4.8  Editorial Activities

  1. From 2000 to 2008, Implementation Area Editor and responsible for the Net Talk section of the ALP newsletter, the bulletin of the Association for Logic Programming.

4.9  Referee Activity for International Journals

  1. Journal of Logic Programming;
  2. Journal of Functional and Logic Programming;
  3. Information Processing Letters;
  4. Theory and Practice of Logic Programming;
  5. Theoretical Computer Science.
  6. Journal of Automated Reasoning.
  7. ACM Transactions on Computational Logic.
  8. Science of Computer Programming;

4.10  Referee Activity for International Conferences

  1. GULP’93, “Ottavo Convegno sulla Programmazione Logica”, Gizzeria Lido, Italy, June 1993.
  2. AMAST’93, “Algebraic Methodology and Software Technology”, Enschede, Nederland, June 1993.
  3. WSA’93, “3rd International Workshop on Static Analysis”, Padua, Italy, September 1993.
  4. ILPS’93, “International Logic Programming Symposium”, Vancouver, British Columbia, Canada, October 1993.
  5. AI*IA’93, “Terzo Congresso dell’Associazione Italiana per l’Intelligenza Artificiale”, Torino, Italy, October 1993.
  6. SAC’94, “ACM Symposium on Applied Computing”, Phoenix, Arizona, USA, March 1994
  7. ICLP’94, “International Conference on Logic Programming”, S. Margherita Ligure, Italy, June 1994.
  8. PLILP’94, “Programming Languages Implementation and Logic Programming”, Madrid, Spain, September 1994.
  9. ALP’94, “Third International Conference on Algebraic and Logic Programming”, Madrid, Spain, September 1994.
  10. GULP-PRODE’94, “Joint Conference on Declarative Programming”, Peñíscola, Spain, September 1994.
  11. SAS’94, “International Static Analysis Symposium”, Namur, Belgium, September 1994.
  12. PLILP’95, “International Symposium on Programming Languages, Implementations, Logics and Programs”, Utrecht, Nederland, September 1995.
  13. ILPS’95, “International Logic Programming Symposium”, Portland, Oregon, USA, December 1995.
  14. ESOP’96, “European Symposium on Programming”, Linköping, Sweden, April 1996.
  15. ECAI’96, “European Conference on Artificial Intelligence” Budapest, Hungary, August 1996.
  16. PLILP’96, “Eighth International Symposium on Programming Languages, Implementations, Logics, and Programs”, Aachen, Germany, September 1996.
  17. SAS’96, “Third International Static Analysis Symposium”, Aachen, Germany, September 1996.
  18. LOPSTR’97, “Seventh International Workshop on Logic Program Synthesis and Transformation”, Leuven, Belgium, July 1997.
  19. JICSLP’98, “Joint International Conference and Symposium on Logic Programming” Manchester, UK, June 1998.
  20. SAS’98, “Fifth International Static Analysis Symposium”, Pisa, Italy, September 1998.
  21. PLILP/ALP’98, “Tenth International Symposium on Programming Languages, Implementations, Logics and Programs” and “Seventh International Conference on Algebraic and Logic Programming”, Pisa, Italy, September 1998.
  22. SAS’99, “International Static Analysis Symposium”, Venice, Italy, September 1999.
  23. PPDP’99, “International Conference on Principles and Practice of Declarative Programming”, Paris, France, September–October 1999.
  24. SAS 2000, “Seventh International Static Analysis Symposium”, Santa Barbara, USA, June–July 2000.
  25. ESSLLI-2000, “Twelfth European Summer School in Logic, Language and Information”, student session, Birmingham, UK, August 2000.
  26. APPIA-GULP-PRODE’00, “2000 Joint Conference on Declarative Programming”, La Havana, Cuba, December 2000.
  27. LPAR 2000, “Seventh International Conference on Logic for Programming and Automated Reasoning”, Réunion Island, Indian Ocean, France, November 2000.
  28. LPAR 2001, “Eighth International Conference on Logic for Programming, Artificial Intelligence and Reasoning”, La Havana, Cuba, December 2001.
  29. SAS’02, “Ninth International Static Analysis Symposium”, Madrid, Spain, September 2002.
  30. ESOP’03, “European Symposium on Programming”, Warsaw, Poland, April 2003.
  31. SAS’03, “Tenth International Static Analysis Symposium”, San Diego, California, USA, June 2003.
  32. PSI’03, “Perspectives of System Informatics”, Novosibirsk, Akademgorodok, Russia, July 2003.
  33. APPIA-GULP-PRODE’03, “2003 Joint Conference on Declarative Programming”, Reggio Calabria, Italy, September 2003.
  34. WLPE’03, “13th Workshop on Logic Programming Environments”, Mumbai, India, December 2003.
  35. VMCAI’04, “Fifth International Conference on Verification, Model Checking and Abstract Interpretation”, Venice, Italy, January 2004.
  36. ESOP’04, “European Symposium on Programming”, Barcelona, Spain, March–April 2004.
  37. SAS’04, “Eleventh International Static Analysis Symposium”, Verona, Italy, August 2004.
  38. CAV’05, “Seventeenth International Conference on Computer Aided Verification”, The University of Edinburgh, Scotland, UK, July 2005.
  39. SAS’05, “Twelfth International Static Analysis Symposium”, London, UK, September 2005.
  40. LOPSTR’05, “International Symposium on Logic-based Program Synthesis and Transformation”, London, UK, September 2005.
  41. ICLP’05, “Twenty First International Conference on Logic Programming”, Barcelona, Spain, October 2005.
  42. LOPSTR 2006, “International Symposium on Logic-based Program Synthesis and Transformation”, S. Servolo, Venice, Italy, July 2006.
  43. POPL 2007, “Thirtyfourth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages”, Nice, France, January 2007.
  44. ESOP’07, “Sixteenth European Symposium on Programming”, Braga, Portugal, March, 2007.
  45. SAS 2007, “Fourteenth International Static Analysis Symposium”, Kongens Lyngby, Denmark, August 2007.
  46. SAC 2008, “Twentythird Annual ACM Symposium on Applied Computing”, Technical Track on Software Verification, Fortaleza, Ceará, Brasil, March 2008.
  47. VMCAI 2008, “Nineth International Conference on Verification, Model Checking, and Abstract Interpretation”, San Francisco, USA, January 2008.
  48. SAS 2008, “Fifteenth International Static Analysis Symposium”, Valencia, Spain, July 2008.

4.11  Participation to and Coordination of Research Projects

4.11.1  Current and Past Projects

  1. Participant to the ESPRIT Basic Research Action Project n. 6707, “ParForce”.
  2. Participant to the italian national project on “Automatic Program Certification by Abstract Interpretation” (1999–2001, national coordinator: Prof. Roberto Giacobazzi, University of Verona).
  3. Participant to the italian national project on “Abstract Interpretation, Type Systems and Control-Flow Analysis” (2000–2002, national coordinator: Prof. Giorgio Levi, University of Pisa).
  4. Coordinator for Italy of the bilateral project on “Advanced Development Environments for Logic Programs” (Azioni Integrate Italia-Spagna 2001, code IT229, 2001–2003, coordinator for Spain: Prof. Germán Puebla Sánchez, Facultad de Informática, Universidad Politécnica de Madrid).
  5. Participant to the italian national project on “Aggregate- and Number-Reasoning for Computing: from Decision Algorithms to Constraint Programming with Multisets, Sets, and Maps” (2001–2003, national coordinator: Prof. Domenico Cantone, University of Catania).
  6. Coordinator of the Parma research unit for the italian national project on “Constraint-Based Verification of Reactive Systems” (2002–2004, national coordinator: Prof. Maurizio Gabbrielli, University of Bologna).
  7. Italian coordinator for the Royal Society International Joint Project 2004/R1 Europe (ESEP) “Automatic Detection of Unstable Numerical Computations” (2004–2006, main coordinator: Dr Patricia M. Hill, University of Leeds, UK).
  8. Coordinator of the Parma research unit for the italian national project on “AIDA — Abstract Interpretation: Design and Applications” (2004–2006, national coordinator: Prof. Roberto Giacobazzi, University of Verona).
  9. Coordinator of the University of Parma research unit in the ITEA (Information Technology for European Advancement) GlobalGCC project (GGCC), among whose objective was the one of extending the GNU Compiler Collection (GCC) with global static analysis techniques.
  10. Coordinator of the Parma research unit for the italian national project on “AIDA2007 — Abstract Interpretation: Design and Applications” (2008–2010, national coordinator: Prof. Francesco Ranzato, University of Padova).

4.11.2  Project Proposals

  1. Participant, as national representative for Italy and coordinator (with François Irigoin, École des Mines de Paris) of the workpackage on Numerical Abstract Domains, to the proposal IST (VI programma quadro) titled “AINoE: Network of Excellence on Abstract Interpretation” (004456).
  2. Coordinator of the University of Parma research unit in the ITEA2 (Information Technology for European Advancement) project proposal SAFE-GCC (Static Analysis Free & Everywhere for GCC). Partners: ADACORE, Bertin Technologies, CEA LIST, Fundació European Software Institute (ESI), META, NXP Semiconductors, THALES Communications France, Universidad Politécnica de Madrid, Universidad de Las Palmas, Open Sistemas, VTT Technical Research Centre of Finland.

5  Publications

[]
The publications listed here, with the exception of some technical reports, are available at http://www.cs.unipr.it/ bagnara/. Most technical reports are available at http://www.cs.unipr.it.

5.1  International Journals

[1]
Bagnara, R. A unified proof for the convergence of Jacobi and Gauss-Seidel methods. SIAM Review 37, 1 (1995), 93–97.
[2]
Bagnara, R. A hierarchy of constraint systems for data-flow analysis of constraint logic-based languages. Science of Computer Programming 30, 1–2 (1998), 119–155.
[3]
Bagnara, R., Hill, P. M., and Zaffanella, E. Set-sharing is redundant for pair-sharing. Theoretical Computer Science 277, 1-2 (2002), 3–46.
[4]
Hill, P. M., Bagnara, R., and Zaffanella, E. Soundness, idempotence and commutativity of set-sharing. Theory and Practice of Logic Programming 2, 2 (2002), 155–201.
[5]
Zaffanella, E., Hill, P. M., and Bagnara, R. Decomposing non-redundant sharing by complementation. Theory and Practice of Logic Programming 2, 2 (2002), 233–261.
[6]
Hill, P. M., Zaffanella, E., and Bagnara, R. A correct, precise and efficient integration of set-sharing, freeness and linearity for the analysis of finite and rational tree languages. Theory and Practice of Logic Programming 4, 3 (2004), 289–323.
[7]
Bagnara, R., Gori, R., Hill, P. M., and Zaffanella, E. Finite-tree analysis for constraint logic-based languages. Information and Computation 193, 2 (2004), 84–116.
[8]
Bagnara, R., Zaffanella, E., and Hill, P. M. Enhanced sharing analysis techniques: A comprehensive evaluation. Theory and Practice of Logic Programming 5, 1&2 (2005), 1–43.
[9]
Mesnard, F., and Bagnara, R. cTI: A constraint-based termination inference tool for ISO-Prolog. Theory and Practice of Logic Programming 5, 1&2 (2005), 243–257.
[10]
Bagnara, R., Hill, P. M., Ricci, E., and Zaffanella, E. Precise widening operators for convex polyhedra. Science of Computer Programming 58, 1–2 (2005), 28–56.
[11]
Bagnara, R., Hill, P. M., and Zaffanella, E. Not necessarily closed convex polyhedra and the double description method. Formal Aspects of Computing 17, 2 (2005), 222–257.
[12]
Bagnara, R., Hill, P. M., and Zaffanella, E. Widening operators for powerset domains. Software Tools for Technology Transfer 8, 4/5 (2006), 449–466.
[13]
Bagnara, R., Hill, P. M., and Zaffanella, E. The Parma Polyhedra Library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Science of Computer Programming 72, 1–2 (2008), 3–21.
[14]
Bagnara, R., Hill, P. M., and Zaffanella, E. Applications of polyhedral computations to the analysis and verification of hardware and software systems. Theoretical Computer Science 410, 46 (2009), 4672–4691.
[15]
Bagnara, R., Hill, P. M., and Zaffanella, E. Weakly-relational shapes for numeric abstractions: Improved algorithms and proofs of correctness. Formal Methods in System Design 35, 3 (2009), 279–323.
[16]
Bagnara, R., Hill, P. M., and Zaffanella, E. Exact join detection for convex polyhedra and other numerical abstractions. To appear on Computational Geometry: Theory and Applications 43, 5 (2010), 453–473.
[17]
Bagnara, R., Mesnard, F., Pescetti, A., and Zaffanella, E. A new look at the automatic synthesis of linear ranking functions. Information and Computation 215 (2012), 47–67.
[18]
Covington, M. A., Bagnara, R., O’Keefe, R. A., Wielemaker, J., and Price, S. Coding guidelines for Prolog. Theory and Practice of Logic Programming 12, 6 (2012), 889–927.

5.2  Proceedings of International Conferences

[19]
Perrin, Y., Bagnara, R., Berners-Lee, T. J., Carena, W., Divia, R., Parkman, C., Petersen, J., Tremblet, L., and Wessels, B. The valet-plus embedded into large physics experiments. In Proceedings of the “VMEbus in Research International Conference” (Zürich, Oct. 1988), C. Eck and C. Parkman, Eds., Elsevier Science Publishers B.V. (North-Holland), Amsterdam, pp. 59–68.
[20]
Heyes, G., Wessels, B., Perrin, Y., Bagnara, R., Berners-Lee, T. J., Carena, W., Divia, R., Parkman, C., Petersen, J., and Tremblet, L. The integration of vax and valet-plus data acquisition software. Contribution to the “Sixth Conference on Real-Time Computer Applications in Nuclear, Particle, and Plasma Physics” (Williamsburg, VA, May 1989). IEEE Transactions on Nuclear Science 36, 5 (1989), 1572–1576.
[21]
Bagnara, R., Giacobazzi, R., and Levi, G. An application of constraint propagation to data-flow analysis. In Proceedings of “The Ninth Conference on Artificial Intelligence for Applications” (Orlando, Florida, March 1993), IEEE Computer Society Press, Los Alamitos, CA, pp. 270–276.
[22]
Bagnara, R. A reactive implementation of Pos using ROBDDs. In Programming Languages: Implementations, Logics and Programs, Proceedings of the Eighth International Symposium (Aachen, Germany, 1996), H. Kuchen and S. D. Swierstra, Eds., vol. 1140 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, pp. 107–121.
[23]
Bagnara, R., Hill, P. M., and Zaffanella, E. Set-sharing is redundant for pair-sharing. In Static Analysis: Proceedings of the 4th International Symposium (École Normale Supérieure, Paris, France, 1997), P. Van Hentenryck, Ed., vol. 1302 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, pp. 53–67.
[24]
Hill, P. M., Bagnara, R., and Zaffanella, E. The correctness of set-sharing. In Static Analysis: Proceedings of the 5th International Symposium (Pisa, Italy, 1998), G. Levi, Ed., vol. 1503 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, pp. 99–114.
[25]
Bagnara, R., and Schachte, P. Factorizing equivalent variable pairs in ROBDD-based implementations of Pos. In Proceedings of the “Seventh International Conference on Algebraic Methodology and Software Technology (AMAST’98)” (Amazonia, Brazil, 1999), A. M. Haeberer, Ed., vol. 1548 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, pp. 471–485.
[26]
Zaffanella, E., Bagnara, R., and Hill, P. M. Widening Sharing. In Principles and Practice of Declarative Programming (Paris, France, 1999), G. Nadathur, Ed., vol. 1702 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, pp. 414–431.
[27]
Zaffanella, E., Hill, P. M., and Bagnara, R. Decomposing non-redundant sharing by complementation. In Static Analysis: Proceedings of the 6th International Symposium (Venice, Italy, 1999), A. Cortesi and G. Filé, Eds., vol. 1694 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, pp. 69–84.
[28]
Bagnara, R., Zaffanella, E., and Hill, P. M. Enhanced sharing analysis techniques: A comprehensive evaluation. In Proceedings of the 2nd International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (Montreal, Canada, 2000), M. Gabbrielli and F. Pfenning, Eds., Association for Computing Machinery, pp. 103–114.
[29]
Bagnara, R., Hill, P. M., and Zaffanella, E. Efficient structural information analysis for real CLP languages. In Proceedings of the 7th International Conference on Logic for Programming and Automated Reasoning (LPAR 2000) (Reunion Island, France, 2000), M. Parigot and A. Voronkov, Eds., vol. 1955 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, pp. 189–206.
[30]
Bagnara, R., Gori, R., Hill, P. M., and Zaffanella, E., Finite-tree analysis for constraint logic-based languages, In Static Analysis: Proceedings of the 8th International Symposium (SAS 2001), (Paris, France, 2001), P. Cousot, Ed., vol. 2126 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, pp. 165–184.
[31]
Bagnara, R., Zaffanella, E., Gori, R., and Hill, P. M. Boolean functions for finite-tree dependencies. In Proceedings of the 8th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2001) (Havana, Cuba, 2001), R. Nieuwenhuis and A. Voronkov, Eds., vol. 2250 of Lecture Notes in Artificial Intelligence, Springer-Verlag, Berlin, pp. 575–589.
[32]
Bagnara, R., Ricci, E., Zaffanella, E., and Hill, P. M. Possibly not closed convex polyhedra and the Parma Polyhedra Library. In Static Analysis: Proceedings of the 9th International Symposium (Madrid, Spain, 2002), M. V. Hermenegildo and G. Puebla, Eds., vol. 2477 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, pp. 213–229.
[33]
Bagnara, R., Hill, P. M., Ricci, E., and Zaffanella, E. Precise widening operators for convex polyhedra. In Static Analysis: Proceedings of the 10th International Symposium (San Diego, California, USA, 2003), R. Cousot, Ed., vol. 2694 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, pp. 337–354.
[34]
Bagnara, R., Hill, P. M., and Zaffanella, E. Widening operators for powerset domains. In Proceedings of the Fifth International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI 2004) (Venice, Italy, 2003), B. Steffen and G. Levi, Eds., vol. 2937 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, pp. 135–148.
[35]
Bagnara, R., Hill, P. M., Mazzi, E., and Zaffanella, E. Widening operators for weakly-relational numeric abstractions. In Static Analysis: Proceedings of the 12th International Symposium (London, UK, 2005), C. Hankin, Ed., Lecture Notes in Computer Science, Springer-Verlag, Berlin.
[36]
Bagnara, R., Rodríguez-Carbonell, E., and Zaffanella, E. Generation of basic semi-algebraic invariants using convex polyhedra. In Static Analysis: Proceedings of the 12th International Symposium (London, UK, 2005), C. Hankin, Ed., Lecture Notes in Computer Science, Springer-Verlag, Berlin.
[37]
Bagnara, R., Dobson, K., Hill, P. M., Mundell, M., and Zaffanella, E. Grids: A domain for analyzing the distribution of numerical values. In Logic-based Program Synthesis and Transformation, 16th International Symposium (Venice, Italy, 2007), G. Puebla, Ed., vol. 4407 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, pp. 219–235.
[38]
Bagnara, R., Hill, P. M., and Zaffanella, E. An improved tight closure algorithm for integer octagonal constraints. In Verification, Model Checking and Abstract Interpretation: Proceedings of the 9th International Conference (VMCAI 2008) (San Francisco, USA, 2008), F. Logozzo, D. Peled, and L. Zuck, Eds., vol. 4905 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, pp. 8–21.
[39]
Bagnara, R., Carlier, M., Gori, R., and Gotlieb, A. Symbolic path-oriented test data generation for floating-point programs. In Proceedings of the 6th IEEE International Conference on Software Testing, Verification and Validation (Luxembourg City, Luxembourg, 2013), IEEE Press.

5.3  Proceedings of International Workshops

[40]
Bagnara, R., Giacobazzi, R., and Levi, G. Static analysis of CLP programs over numeric domains. In Actes “Workshop on Static Analysis ’92” (Bordeaux, September 1992), M. Billaud, P. Castéran, M. Corsini, K. Musumbu, and A. Rauzy, Eds., vol. 81–82 of Bigre, Atelier Irisa, IRISA Campus de Beaulieu, pp. 43–50.
[41]
Bagnara, R. On the detection of implicit and redundant numeric constraints in CLP programs. In Proceedings of the “1994 Joint Conference on Declarative Programming (GULP-PRODE’94)” (Peñíscola, Spain, September 1994), M. Alpuente, R. Barbuti, and I. Ramos, Eds., pp. 312–326.
[42]
Bagnara, R. Constraint systems for pattern analysis of constraint logic-based languages. In Proceedings of the “1995 Joint Conference on Declarative Programming (GULP-PRODE’95)” (Marina di Vietri, Italy, September 1995), M. Alpuente and M. I. Sessa, Eds., pp. 581–592.
[43]
Bagnara, R. Straight ROBDDs are not the best for Pos. In Proceedings of the “1996 Joint Conference on Declarative Programming (APPIA-GULP-PRODE’96)” (Donostia-San Sebastián, Spain, 1996), Lucio, P., Martelli, M., and Navarro, M., Eds., pp. 493–496.
[44]
Bagnara, R., Comini, M., Scozzari, F., and Zaffanella, E. The AND-compositionality of CLP computed answer constraints. In Proceedings of the “1996 Joint Conference on Declarative Programming (APPIA-GULP-PRODE’96)” (Donostia-San Sebastián, Spain, 1996), Lucio, P., Martelli, M., and Navarro, M., Eds., pp. 355–366.
[45]
Bagnara, R. Structural information analysis for CLP languages. In Proceedings of the “1997 Joint Conference on Declarative Programming (APPIA-GULP-PRODE’97)” (Grado, Italy, 1997), Falaschi, M., Navarro, M., and Policriti, A., Eds., pp. 81–92.
[46]
Bagnara, R., Hill, P. M., and Zaffanella, E. Sharing revisited. In Proceedings of the “1997 Joint Conference on Declarative Programming (APPIA-GULP-PRODE’97)” (Grado, Italy, 1997), Falaschi, M., Navarro, M., and Policriti, A., Eds., pp. 69–80.
[47]
Bagnara, R., and Schachte, P. Factorizing equivalent variable pairs in ROBDD-based implementations of Pos. In Proceedings of the “1998 Joint Conference on Declarative Programming (APPIA-GULP-PRODE’98)” (A Coruña, Spain, 1998), Freire-Nistal, J. L., Falaschi, M., and Vilares-Ferro, M., Eds., pp. 227–239.
[48]
Hill, P. M., Bagnara, R., and Zaffanella, E. The correctness of set-sharing. In Proceedings of the “1998 Joint Conference on Declarative Programming (APPIA-GULP-PRODE’98)” (A Coruña, Spain, 1998), Freire-Nistal, J. L., Falaschi, M., and Vilares-Ferro, M., Eds., pp. 255–267.
[49]
Bagnara, R., Zaffanella, E., and Hill, P. M. Enhancing Sharing for precision. In Proceedings of the “APPIA-GULP-PRODE’99 Joint Conference on Declarative Programming” (L’Aquila, Italy, 1999), Meo, M. C., and Ferro, M. V., Eds., pp. 213–227.
[50]
Zaffanella, E., Bagnara, R., and Hill, P. M. Widening Sharing. In Proceedings of the “APPIA-GULP-PRODE’99 Joint Conference on Declarative Programming” (L’Aquila, Italy, 1999), Meo, M. C., and Ferro, M. V., Eds., pp. 559–573.
[51]
Bagnara, R., Hill, P. M., and Zaffanella, E. A new encoding of not necessarily closed convex polyhedra. In Proceedings of the 1st CoLogNet Workshop on Component-based Software Development and Implementation Technology for Computational Logic Systems (Madrid, Spain, 2002), M. Carro, C. Vacheret, and K.-K. Lau, Eds., pp. 147–153. Published as TR Number CLIP4/02.0, Universidad Politécnica de Madrid, Facultad de Informática.
[52]
Bagnara, R., Hill, P. M., and Zaffanella, E. A new encoding and implementation of not necessarily closed convex polyhedra. In Proceedings of the 3rd Workshop on Automated Verification of Critical Systems (Southampton, UK, 2003), M. Leuschel, S. Gruner, and S. Lo Presti, Eds., pp. 161–176. Published as TR Number DSSE-TR-2003-2, University of Southampton.
[53]
Bagnara, R., Hill, P. M., Pescetti, A., and Zaffanella, E. Verification of C programs via natural semantics and abstract interpretation. In Proceedings of the C/C++ Verification Workshop (Oxford, UK, 2007), H. Tews, Ed., pp. 75–80. Extended abstract. Published as Technical Report ICIS–R07015, Institute for Computing and Information Sciences (iCIS), Radboud University Nijmegen, Nijmegen, The Netherlands.
[54]
Bagnara, R., Hill, P. M., and Zaffanella, E. A Prolog-based environment for reasoning about programming languages. Tech. Rep. arXiv:cs.PL/0711.0345, Dipartimento di Matematica, Università di Parma, Italy, 2007. Extended abstract. Contribution to the 17th International Workshop on “Logic-based methods in Programming Environments” (WLPE’07, Porto, Portugal, September 13, 2007). Available from http://arxiv.org/.
[55]
Alezan, A., Bagnara, R., Mesnard, F., and Payet, E. Détection des fonctions de rang linéaires à terme. In Actes des Neuvièmes Journées Francophones de Programmation par Contraintes (JFPC 2013) (Aix-en-Provence, France, 2013), pp. 11–20. In French.

5.4  Edited Books

[56]
Bagnara, R., and Macchi Jánica, G., Eds. Open Source, Free Software e Open Format nei processi di ricerca archeologici (Atti del I Workshop) (2007), Centro Editoriale Toscano, Firenze.

5.5  Ph.D. Thesis

[57]
Bagnara, R. Data-Flow Analysis for Constraint Logic-Based Languages. PhD thesis, Dipartimento di Informatica, Università di Pisa, Corso Italia 40, I-56125 Pisa, Italy, Mar. 1997. Printed as Report TD-1/97.

5.6  Technical Reports

[58]
Bagnara, R., Hill, P. M., and Zaffanella, E. Sharing revisited. Tech. Rep. 97.19, School of Computer Studies, University of Leeds, U.K., 1997.
[59]
Bagnara, R., Hill, P. M., and Zaffanella, E. Set-sharing is redundant for pair-sharing. Quaderno 172, Dipartimento di Matematica, Università di Parma, Italy, 1998. Available at http://www.cs.unipr.it/Publications/.
[60]
Zaffanella, E., Bagnara, R., and Hill, P. M. Widening set-sharing. Quaderno 188, Dipartimento di Matematica, Università di Parma, 1999.
[61]
Zaffanella, E., Hill, P. M., and Bagnara, R. Decomposing non-redundant sharing by complementation. Tech. Rep. 99.07, School of Computer Studies, University of Leeds, U.K., 1999.
[62]
Bagnara, R., Hill, P. M., and Zaffanella, E. Efficient structural information analysis for real CLP languages. Quaderno 229, Dipartimento di Matematica, Università di Parma, 2000. Available at http://www.cs.unipr.it/ bagnara/.
[63]
Bagnara, R., Gori, R., Hill, P. M., and Zaffanella, E., Finite-tree analysis for constraint logic-based languages, Quaderno 251, Dipartimento di Matematica, Università di Parma, 2001. Available at http://www.cs.unipr.it/ bagnara/.
[64]
Bagnara, R., Zaffanella, E., Gori, R., and Hill, P. M., Boolean functions for finite-tree dependencies, Quaderno 252, Dipartimento di Matematica, Università di Parma, 2001. Available at http://www.cs.unipr.it/ bagnara/.
[65]
Hill, P. M., Zaffanella, E., and Bagnara, R. A correct, precise and efficient integration of set-sharing, freeness and linearity for the analysis of finite and rational tree languages. Quaderno 273, Dipartimento di Matematica, Università di Parma, Italy, 2001. Available at http://www.cs.unipr.it/Publications/. Also published as technical report No. 2001.22, School of Computing, University of Leeds, U.K.
[66]
Bagnara, R., and Carro, M. Foreign language interfaces for Prolog: A terse survey. Quaderno 283, Dipartimento di Matematica, Università di Parma, Italy, 2002. Version 1. Available at http://www.cs.unipr.it/Publications/.
[67]
Bagnara, R., Dobson, K., Hill, P. M., Mundell, M.,and Zaffanella, E. A linear domain for analyzing the distribution of numerical values. Tech. Rep. 2005.06, School of Computing, University of Leeds, U.K., 2005.
[68]
Bagnara, R., Ricci, E., Zaffanella, E., and Hill, P. M. Possibly not closed convex polyhedra and the Parma Polyhedra Library. Quaderno 286, Dipartimento di Matematica, Università di Parma, Italy, 2002. Available at http://www.cs.unipr.it/Publications/.
[69]
Bagnara, R., Hill, P. M., and Zaffanella, E. A new encoding and implementation of not necessarily closed convex polyhedra. Quaderno 305, Dipartimento di Matematica, Università di Parma, Italy, 2002. Available at http://www.cs.unipr.it/Publications/.
[70]
Hill, P. M., Zaffanella, E., and Bagnara, R. On the analysis of set-sharing, freeness and linearity for finite and rational tree languages. Tech. Rep. 2003.08, School of Computing, University of Leeds, U.K., 2003.
[71]
Bagnara, R., Hill, P. M., Ricci, E., and Zaffanella, E. Precise widening operators for convex polyhedra. Quaderno 312, Dipartimento di Matematica, Università di Parma, Italy, 2003. Available at http://www.cs.unipr.it/Publications/.
[72]
Bagnara, R., Zaccagnini, A., and Zolo, T. The automatic solution of recurrence relations. I. Linear recurrences of finite order with constant coefficients. Quaderno 334, Dipartimento di Matematica, Università di Parma, Italy, 2003. Available at http://www.cs.unipr.it/Publications/.
[73]
Bagnara, R., and Zaccagnini, A. Checking and bounding the solutions of some recurrence relations. Quaderno 344, Dipartimento di Matematica, Università di Parma, Italy, 2004. Available at http://www.cs.unipr.it/Publications/.
[74]
Bagnara, R., Hill, P. M., and Zaffanella, E. Widening operators for powerset domains. Quaderno 349, Dipartimento di Matematica, Università di Parma, Italy, 2004. Available at http://www.cs.unipr.it/Publications/.
[75]
Bagnara, R., Gori, R., Hill, P. M., and Zaffanella, E. Finite-tree analysis for constraint logic-based languages: the complete unabridged version. Quaderno 363, Dipartimento di Matematica, Università di Parma, Italy, 2004. Available at http://www.cs.unipr.it/Publications/.
[76]
Bagnara, R., Hill, P. M., Mazzi, E., and Zaffanella, E. Widening operators for weakly-relational numeric abstractions. Report arXiv:cs.PL/0412043, 2004. Extended abstract. Contribution to the International workshop on “Numerical & Symbolic Abstract Domains” (NSAD’05, Paris, January 21, 2005). Available at http://arxiv.org/ and http://bugseng.com/products/ppl.
[77]
Bagnara, R., Hill, P. M., Mazzi, E., and Zaffanella, E. Finite-tree analysis for constraint logic-based languages: the complete unabridged version. Quaderno 399, Dipartimento di Matematica, Università di Parma, Italy, 2005. Available at http://www.cs.unipr.it/Publications/.
[78]
Bagnara, R., Rodríguez-Carbonell, E., and Zaffanella, E. Generation of basic semi-algebraic invariants using convex polyhedra. Report de recerca LSI-05-14-R, Departament de Llenguatges i Sistemes Informàtics, Universitat Politècnica de Catalunya, Barcelona, Spain, 2005. Available at http://www.lsi.upc.edu/dept/techreps/techreps.html.
[79]
Bagnara, R., Hill, P. M., and Zaffanella, E. The Parma Polyhedra Library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Quaderno 457, Dipartimento di Matematica, Università di Parma, Italy, 2006. Available at http://www.cs.unipr.it/Publications/. Also published as arXiv:cs.MS/0612085, available from http://arxiv.org/.
[80]
Bagnara, R., Hill, P. M., and Zaffanella, E. Applications of polyhedral computations to the analysis and verification of hardware and software systems. Quaderno 458, Dipartimento di Matematica, Università di Parma, Italy, 2007. Available at http://www.cs.unipr.it/Publications/. Also published as arXiv:cs.CG/0701122, available from http://arxiv.org/.
[81]
Bagnara, R., Hill, P. M., and Zaffanella, E. An improved tight closure algorithm for integer octagonal constraints. Quaderno 467, Dipartimento di Matematica, Università di Parma, Italy, 2007. Available at http://www.cs.unipr.it/Publications/. Also published as arXiv:0705.4618v2 [cs.DS], available from http://arxiv.org/.
[82]
Bagnara, R., Hill, P. M., Pescetti, A., and Zaffanella, E. On the design of generic static analyzers for imperative languages. Quaderno 485, Dipartimento di Matematica, Università di Parma, Italy, 2008. Available at http://www.cs.unipr.it/Publications/.
[83]
Bagnara, R., Hill, P. M., and Zaffanella, E. Exact join detection for convex polyhedra and other numerical abstractions. Quaderno 492, Dipartimento di Matematica, Università di Parma, Italy, 2009. Available at http://www.cs.unipr.it/Publications/. Also published as arXiv:0904.1783v2 [cs.CG], available from http://arxiv.org/.
[84]
Bagnara, R., Mesnard, F., Pescetti, A., and Zaffanella, E. The automatic synthesis of linear ranking functions: The complete unabridged version. Quaderno 498, Dipartimento di Matematica, Università di Parma, Italy, 2010. Available at http://www.cs.unipr.it/Publications/. Also published as arXiv:cs.PL/1004.0944, available from http://arxiv.org/.

5.7  Other Writings

[85]
Bagnara, R. Announcing Kermit68K, a Portable 68000 Kermit Program. Info-Kermit Digest 6, 15 (July 1987).
[86]
Bagnara, R. A General Event Handling System for the Valet-Plus. CERN Data Handling Division, Online Computing Group, September 1988.
[87]
Bagnara, R. Remote Procedure Call. CERN Mini & Micro Computer Newsletter 20 (October 1988).
[88]
Bagnara, R. Interpretazione astratta di linguaggi logici con vincoli su domini finiti. M.Sc. dissertation, University of Pisa, July 1992. In Italian.
[89]
Bagnara, R. Analysing with China. The Association for Logic Programming Newsletter 12, 1 (1999), 9.
[90]
Bagnara, R. Is the ISO Prolog standard taken seriously? The Association for Logic Programming Newsletter 12, 1 (1999), 10–12.
[91]
Bagnara, R. On the quality of available Prolog implementations. The Association for Logic Programming Newsletter 12, 2 (1999), 12–14.
[92]
Bagnara, R. Precise and Practical Mode Analysis with the China Analyzer. Computational Logic 7, November 1999.
[93]
Bagnara, R., Hill, P. M., and Zaffanella, E. The Parma Polyhedra Library User’s Manual, release 1.0 ed. BUGSENG srl, Parma, Italy, June 2012. Available at http://bugseng.com/products/ppl.

5.8  Recent Software

Most of the theoretical research work has been validated and, in some cases, inspired by the design and development of software systems that implement or use abstract interpretation techniques for program analysis. All the software projects mentioned in this section are coordinated by Roberto Bagnara.

5.8.1  PPL

The PPL (Parma Polyhedra Library is a software library for the representation and manipulation of numerical abstractions especially targeted at applications concerning the analysis and verification of software and hardware (digital and/or analog) systems. The library supports abstractions based not necessarily closed (NNC) convex polyhedra, rational grids, a wide selection of difference and octagonal shapes, the most powerful and wide family of intervals available in the free software world (closed intervals, possibly non-closed ones, with boundaries given by any native integral or floating point type, unbounded integers or rationals, possibly with restrictions like modulo interval and strided interval), plus products and finite powersets of the above. The PPL has several features that make it unique: these include a natural interface for NNC polyhedra, innovative widening operators and support for time- and memory-bounded computations. The Parma Polyhedra Library provides several user friendly interfaces (C++, C, Java, OCaml and Prolog); it is fully dynamic (available virtual memory is the only limitation to the dimension of anything); it is portable (written in standard C++ and following all other available standards); it is exception-safe (never leaks resources or leaves invalid object fragments around); it is quite efficient and thoroughly documented. The library is free software distributed under the terms of the GNU General Public License. For the most up-to-date information, documentation and downloads and to follow the development work see the Parma Polyhedra Library site at http://bugseng.com/products/ppl. The PPL is used by many projects and by the most prestigious research centers in the field of formal analysis and verification. In particular, it is used by GCC —the GNU Compiler Collection—, probably the compilers’ suite in most widespread use.

5.8.2  ECLAIR

ECLAIR is a new, professional platform for the verification of the C family of languages. It can currently analyze several dialects of C, but work on extending ECLAIR to C++ has already started. The main features of the current version of ECLAIR are summarized in the following paragraphs.

Toolchain Emulation and Unchanged Build System

A powerful and completely generic option-processing mechanism allows ECLAIR to masquerade as any toolchain component, such as gcc, with its 1000+ options, and any other compiler, assembler and linker. Thanks to this kind of mimicry, ECLAIR can access all the code comprising an application or library without requiring any change in the build system. In particular, if the application/library can be built in parallel (e.g., via make -j), then it can be analyzed with ECLAIR in parallel. Here, for instance, is how httpd version 2.2.11 can be analyzed once the verification tasks to be performed have been specified in the file my_setup: 

$ tar jxf httpd-2.2.11.tar.bz2
$ cd httpd-2.2.11
$ ./configure
$ eclair_env -eval-file=my_setup -- make -j 6

Double AST Interface

The ECLAIR parser builds an abstract syntax tree (AST) that is available to the other components of the system via two different, though completely interoperable, interfaces: (1) As a Prolog term that directly encodes all and only the syntactic aspects of the program; but incorporating “handles” as subterms that give easy access to all non-syntactic information. (2) As a number of inter-related C++ classes: a more complex representation that, however, gives access to all the information. The Prolog view makes it easy to code syntax-based algorithms, such as coding rule checkers, program analyzers and transformers.

Precise and Fast Parsing

The AST built by the parser encodes precise information about the original source code so that we can recover, almost for each token, complete information on the chain of file inclusions and, orthogonally, the chain of macro expansions that brought it to the preprocessed source. This means that we can build tools able to identify the precise points in the source that are responsible for a given state of affairs. The parser, which supports ISO C90 and C99 along with several GNU and Microsoft extensions, is pretty fast: today running at more than 100,000 lines of code per second, with room for further optimizations.

Simplified Intermediate Form

ECLAIR includes a semantics-preserving program transformer that can simplify a program into a subset of C (or C++), the main simplification consisting of the removal of side-effects from expressions. The simplified form, which is of course compilable and semantically equivalent, makes it much easier to develop semantics-based program manipulations.

Coding Rule Checkers and Bug Finders

The coding rule checkers support the following rule sets: MISRA-C:2004, CERT C Secure Coding Standard, JSF C++, High-Integrity C++. The simplicity and elegance with which checkers can be defined is available to users that wish to develop their own checkers.

Precise and Scalable Program Analysis

We are porting the semantic analysis engine of a previous prototype to ECLAIR. This includes a flow-, context- and field-sensitive pointer analysis along with numerical value analyses based on the Parma Polyhedra Library, a state-of-the-art library of numerical abstractions. A key feature of ECLAIR will be reduction of false positives thanks to sophisticated program analyses and not via the introduction of false negatives.

5.8.3  PURRS

Purrs (Parma University’s Recurrence Relation Solver is a prototype of an automatic recurrence relation solver. It is able to automatically solve difference equation and other generalized recurrences providing, when possible, a closed formula (i.e., a formula containing a number of ‘+’ or ‘−’ signs that is independent of the main variable). If Purrs fails to find such a closed formula, it will express the solution, whenever possible, in terms of sums and/or products. A closed formula (or its generalization involving symbolic sums and products) is guaranteed to exist only in rather special circumstances, and in general Purrs will only find upper and lower bounds for the solution of the recurrence. Notice that these are proper upper and lower bounds, which are valid for all possible inputs, rather than asymptotic bounds. This possibility is a first step toward the definition of an automatic complexity analysis of programs that is able to provide real guarantees concerning resource usage. Purrs is free software distributed under the terms of the GNU General Public License. All the information is available at http://www.cs.unipr.it/purrs/. At the same URI, an interactive prototype is available that allows to explore the capabilities of the system.

5.8.4  CHINA

China (Clp(H, N) Analyzer) is a parametric static analyzer for (constraint) logic programming languages. The analyzer accepts ISO Prolog programs and uses several abstract domains that allow to determine approximations of the following information concerning program variables and terms bound to them: groundness, sharing, freeness, linearity, compoundness, shape, finiteness, simple types, values of the numerical leaves, and linear relations among term sizes.

5.8.5  OCRA

Ocra (Occur-Check Reduction Analyzer) is a prototype using the information provided by the China analyzer for the occur-check reduction of logic languages. Given, e.g., an ISO Prolog program, Ocra produces a new ISO Prolog program that can be correctly executed even on systems that omit the occur-check in the unification procedure.

5.8.6  CLAIR

The CLAIR (Combined Language and Abstract Interpretation Resource) system has been developed in order to study and experiment with various aspects of programming language implementation. In particular it is aimed to provide easy ways of playing with: (1) lexical analysis; (2) syntactic analysis and generation of the abstract syntax tree (parsing); (3) static checking of type correctness; (4) operational semantics expressed by means of transition systems; (5) interpretation; (6) static analysis; (7) compilation. Points 1–5 are fully developed; point 6 has been implemented, but further development has moved to the new ECLAIR system; point 7 has been investigated in some small student projects. The CLAIR approach is based on structured operational semantics à la Plotkin for the formal description and on the Prolog language for the implementation. One of the advantages of this combined approach is that it is relatively easy to extend the system so as to support other language features. CLAIR is currently being used successfully in university courses covering formal languages and operational semantics.1 Its main advantage is that students can see, with relatively little effort, theory at work: a grammar becomes a parser; static semantics rules directly translate into a type checker; concrete dynamic semantics rules result in an interpreter for the language; abstract dynamic rules can be turned into a static program analyzer. More information is available at http://www.cs.unipr.it/clair/.

1
Analysis and Verification of Software, degree in “Informatica”, University of Parma, Italy; Programming Language Semantics (CS31), School of Computing, University of Leeds, UK.

[Page last updated on July 05, 2013, 17:06:08.]

© Roberto Bagnara
bagnara@cs.unipr.it

Home | Personal | Papers | Teaching | Links