
Curriculum Vitae et Studiorum of Roberto Bagnara
CURRICULUM VITAE ET STUDIORUM
CURRICULUM VITAE ET STUDIORUMRoberto Bagnara 
ContentsCurriculum vitae et studiorum of Roberto Bagnara
1 Personal DataSurname:  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 AddressesWork:  Department of Mathematics and Computer Science 
 University of di Parma 
 Parco Area delle Scienze 53/A 
 I43124 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 positionFull professor of Computer Science
(Informatica)
at the Department of Mathematics and Computer Science
of the University of Parma, Italy.
1.3 Degrees
Nongraduate 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 writtenEnglish (advanced), French (advanced) and Spanish (intermediate).
2 Curriculum vitae et studiorum 1978–1982:
 Nongraduate 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 spinoff 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 TaughtAll the activities listed in this section refer to courses of studies
of the University of Parma. 
“Informatica” (Computer Science),
degree in “Biotechnologies”,
academic years 19992000 and 20002001.
 “Laboratorio di informatica” (Laboratory of Computer Science),
degree in “Mathematics”,
academic year 20002001.
 “Programmazione (metodi avanzati)” (Advanced Programming Techniques),
degree in “Mathematics”,
academic years 20002001 and 20022003.
 “Programmazione 3” (3rd course on Programming),
degrees in “Mathematics” and “Mathematics and Computer Science”,
academic year 20022003.
 “Scrittura matematica e informatica”
(Writing for Mathematics and Computer Science),
degrees in “Mathematics” and “Mathematics and Computer Science”,
academic year 20022003.
 “Programmazione I” (1st course on Programming),
degrees in “Mathematics”,
“Mathematics and Computer Science”
e “Mathematics for Technology and Finance”,
academic year 20012002.
 “Fondamenti dell’informatica” (Foundations of Computer Science),
degrees in “Mathematics” e
“Mathematics and Computer Science”,
academic years 20022003, 20032004, 20042005, 20062007, 20072008,
20082009, 20092010, 20102011, 20112012 and 20122013.
 “Fondamenti dell’informatica” (Foundations of Computer Science),
degree in “Computer Science”,
academic years 20022003, 20032004, 20052006, 20062007, 20072008,
20082009, 20092010, 20102011, 20112012 and 20122013.
 “Scrittura matematica e informatica”
(Writing for Mathematics and Computer Science),
degree in “Computer Science”,
academic years 20032004, 20042005 and 20052006.
 “Linguaggi di programmazione”
(Programming Languages),
degree in “Computer Science”,
academic year 20062007, 20072008, 20082009, 20092010 and 20102011.
 “Analisi e verifica del software”
(Analysis and Verification of Software),
degree in “Computer Science”,
academic years 20032004, 20042005, 20052006, 20062007, 20072008, 20082009.
 “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 20062007.
 “Algorithmique” (Algorithmics),
Licence de mathématiques,
Université de la Réunion,
academic year 20062007.
 “Laboratorio di informatica” (Laboratory of Computer Science),
Degree in “Environmental Sciences”,
University of Siena, Follonica (GR),
academic year 20072008.

“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 20092010.
 “Semantica dei linguaggi di programmazione”
(Semantics of Programming Languages),
degree in “Computer Science”,
academic years 20102011, 20112012 e 20122013.
3.2 Teaching Collaborations Lectures (8 hours) on
The Compilation of Prolog and the Warren Abstract Machine
in the course on “Linguaggi speciali di programmazione”
(SpecialPurpose Programming Languages) taught by Prof. Giorgio Levi,
degree in “Computer Science” of the Universityof Pisa,
academic years 19901991, 19911992, 19921993 and 19931994.
 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 19951996,
 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 19971998, 19981999, 19992000 and 20002001.
 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 19981999 and 19992000.
 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 20032004 and 20042005.
3.3 Activity as Advisor and CoAdvisor for M.Sc. (Laurea) Theses
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; coadvisor: R. Bagnara.
University of Pisa.
Academic year 19941995.

Scudellari, M. C.
Analisi bottomup di programmi logici con vincoli basata su
trasformazioni MagicSet
(BottomUp Analysis of Constraint Logic Programs Based on
MagicSet Transformations).
Laurea thesis in “Computer Science”.
Advisor: G. Levi; coadvisor: R. Bagnara.
University of Pisa.
Academic year 19941995.

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; coadvisor R. Bagnara.
University of Pisa.
Academic year 19951996.

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; coadvisor: E. Zaffanella.
Academic year 19992000.

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; coadvisors: C. Medori ed E. Zaffanella.
Academic year 20012002.

Zolo, T.
Risoluzione automatica di relazioni di ricorrenza
(Automatic Solution of Recurrence Relations).
Laurea thesis in “Mathematics”.
University of Parma.
Advisor: R. Bagnara; coadvisors: A. Zaccagnini ed E. Zaffanella.
Academic year 20012002.

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; coadvisor: A. Zaccagnini.
Academic year 20042005.

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; coadvisor: R. Bagnara.
Academic year 20042005.

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; coadvisor: E. Zaffanella.
Academic year 20052005.

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; coadvisor: E. Zaffanella.
Academic year 20052006.

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; coadvisor: E. Zaffanella;
Academic year 20062007.

Soffia, S.
Definizione ed implementazione di una analisi di pointsto
per linguaggi Clike
(Definition and Implementation of a PointsTo Analysis for CLike
Languages).
Laurea thesis in “Computer Science”,
University of Parma.
Advisor: R. Bagnara; coadvisor: E. Zaffanella;
Academic year 20072008.

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 20072008.

Bolzoni, P.
Automatic checking of coding rules.
Laurea thesis in “Computer Science”,
University of Parma.
Advisor: R. Bagnara; coadvisor: E. Zaffanella;
Academic year 20082009.

Poletti, M.
Progettazione ed implementazione di matrici sparse basate su strutture dati cacheoblivious.
(Design and Implementation of Sparse Matrices Based on CacheOblivious Data Structures).
Laurea thesis in “Computer Science”,
University of Parma.
Advisor: E. Zaffanella; coadvisor: R. Bagnara
Academic year 20092010.

Boscolo, A. M.
Un configuratore webbased per un framework di verifica software.
(A WebBased Configurator for a Software Verification Framework).
Laurea thesis in “Computer Science”,
University of Parma.
Advisor: R. Bagnara.
Academic year 20102011.
3.4 Ph.D. Schools 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
GómezZamalloa Gil, M.
Transformación y Análisis de Código de Bytes Orientado a Objetos
(Transformation and Analysis of ObjectOriented Bytecode).
Departamento de Sistemas Informáticos y Computación,
Universidad Complutense de Madrid.
October 2009.

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 Lectures on fundamentals of Computer Science for the specialization
course for highschool teachers of Mathematics organized by
the Faculty of Sciences of the University of Parma,
academic years 19971998 and 19981999.
 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 Technical Student Fellow at CERN
(European Organization for Nuclear Research), Geneva, Switzerland,
January–September 1988.
 Consultant at CERN
(European Organization for Nuclear Research), Geneva, Switzerland,
July–August 1989.
 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.
 Research fellow at the School of Computer Studies
of the University of Leeds, UK,
January–October 1997.
 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.
 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.
 In the framework of the bilateral project on
“Advanced Development Environments for Logic Programs”
(Azioni Integrate ItaliaSpagna 2001, code IT229),
three oneweek 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.
 Visiting scientist at the
Laboratoire d’Informatique
of the
École Polytechnique
(LIX, Paris),
June–July 2008.
 Professeur invité at the
Département de Mathématiques et Informatique
of the Université de La Réunion, S^{t} Denis
(Indian Ocean, France), May 2002, June 2005, May 2006, May 2007,
and March 2010.
4.3 Keynote Speeches Keynote speaker at the
“2011 Meeting
on RichModel 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.
 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 “Introduction to the Warren Abstract Machine”, Dipartimento di Informatica,
University of Pisa, March 1991.
 “DataFlow Analysis for Constraint LogicBased Languages”,
School of Computer Studies, University of Leeds, March 1997.

“Analisis eficiente de informacion estructural para lenguajes
de programacion logica y de restricciones”,
Departamento de Inteligencia Artificial,
Universidad Politécnica de Madrid,
January 2001.
 “Widening Sharing”,
Departamento de Inteligencia Artificial,
Universidad Politécnica de Madrid,
January 2001.
 “The Parma Polyhedra Library”,
Institut de Recherche en Mathématiques et Informatique Appliquées,
Université de La Réunion,
May 2002.
 “Symbolic Computation Support for Complexity Analysis
and the PURRS Project”,
Facultad de Informática,
Universidad Politécnica de Madrid,
May 2003.
 “Convex Polyhedra for the Analysis and Verification
of Hardware and Software Systems: the ‘Parma Polyhedra Library”,
Dipartimento di Matematica,
University of Parma, December 2003.
 “Representation and Manipulation of Not Necessarily Closed Convex Polyhedra”,
Dipartimento di Matematica,
University of Parma, February 2004.
 “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.
 “Analysis and Verification of Software Systems via Abstract Interpretation:
An Informal Introduction”,
Dipartimento di Ingegneria dell’Informazione,
University of Siena,
January 2006.
 “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).
 “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.
 “Numerical Abstract Domains”,
Department of Communication, Business and Information Technologies (CBIT),
Roskilde University,
Roskilde, Denmark,
June 2007.
 “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.
 “On the Design of Generic Static Analyzers for Modern Imperative Languages”,
Facultad de Informática, Universidad Politécnica de Madrid,
Madrid, Spain,
September 2007.
 “Ranking Functions for Automatic Termination Analysis”,
Department of Computer Science, University of Bologna, Italy
December 2007.
 “On the Design of Generic Static Analyzers for Imperative Languages”,
Department of Computer Science, University of Pisa, Italy,
March 2008.
 “Computer Aided Verification of Complex Systems: An Introduction”,
Department of Mathematics, University of Milan, Italy,
March 2008.
 “Numerical Abstract Domains and the Parma Polyhedra Library”,
Department of Computer Science, University of Verona, Italy,
January 2010.
 “Syntactic and Semantic Analysis of SafetyCritical Software”,
Safety Critical Systems Club workshop on
Using the MISRA Guidelines to Support SafetyRelated Systems Development,
Ambassadors Bloomsbury, London, UK,
November 2010.
 “Formal Methods: A Gentle Introduction”,
Atego/HighRely workshop on DO178 & DO254 Avionics Certification,
Milan, Italy
May 2012.

“Une introduction informelle aux méthodes formelles”,
IRILL, Paris,
November 2012.

“The Automatic Synthesis of (Linear) Ranking Functions for Termination Analysis”,
Université Paris Diderot, Paris,
November 2012.
4.5 Program Committees Program Committee member for the
“2000 Joint Conference on Declarative Programming”,
La Habana, Cuba, December 4–7, 2000.
 Program Committee member for the 13th
“Workshop on Logic Programming Environments”,
Mumbai, India, December 8, 2003.
 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,
 Program Committee member for the
“International Symposium on
Logicbased Program Synthesis and Transformation” (LOPSTR’05),
London, UK, September 7–9, 2005.
 Program Committee member for the 21st
“International Conference on Logic Programming” (ICLP’05),
Barcelona, Spain, October 2–5, 2005.
 Program Committee member for the 16th
“International Symposium on
Logicbased Program Synthesis and Transformation” (LOPSTR 2006),
S. Servolo, Venice, Italy, July 12–14, 2006.
 Scientific Committee member of the
Second Workshop on Open Source, Free Software and Open Formats in
Archaeological Research Processes, Genova, Italy, May 11, 2007.
 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.
 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.
 Program Committee member for the 9th “International Conference
on Verification, Model Checking and Abstract Interpretation” (VMCAI 2008),
San Francisco, USA, January 7–9, 2008.
 Program Committee member for the 15th “International Static Analysis
Symposium” (SAS 2008),
Valencia, Spain, July 16–18, 2008.
 Program Committee member for the “Colloquium on Implementation of
Constraint and Logic Programming Systems” (CICLOPS 2008),
Udine, December 12–13, 2008.
 Program Committee member for the 19th
“International Symposium on
Logicbased Program Synthesis and Transformation” (LOPSTR 2009),
Coimbra, Portugal, September 9–11, 2009.
 Scientific Committee member of
ArcheoFOSS 2010,
Foggia, Museo Civico, May 67, 2010.
 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.
 Program Committee member for the
“13th International Conference on Quality Software”
(QSIC 2013),
Nanjing, China, July 29–30, 2013.
 Program Committee member for the
“29th International Conference on Logic Programming”
(ICLP 2013),
Istambul, Turkey, August 24–29, 2013.
 Program Committee member for the
“22nd EACSL Annual Conference on Computer Science Logic”
(CSL 2013),
Turin, Italy, September 2–5, 2013.
 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
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 Workshop Chair for the “Joint International Symposia SAS’98
and PLILPALP’98”,
Pisa, Italy, September 14–18, 1998.
 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/).
 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).
 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/).
 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.
 Scientific Committee member and organizer (with Giancarlo Macchi) of the
IQMDAA Summer School on Quantitative Methods and Data Analysis
in Archaeology, Villa Lanzi, Campiglia Marittima, Italy, September 10–17,
2006.
 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 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 Journal of Logic Programming;
 Journal of Functional and Logic Programming;
 Information Processing Letters;
 Theory and Practice of Logic Programming;
 Theoretical Computer Science.
 Journal of Automated Reasoning.
 ACM Transactions on Computational Logic.
 Science of Computer Programming;
4.10 Referee Activity for International Conferences GULP’93, “Ottavo Convegno sulla Programmazione Logica”,
Gizzeria Lido, Italy,
June 1993.
 AMAST’93, “Algebraic Methodology and Software Technology”,
Enschede, Nederland,
June 1993.
 WSA’93, “3rd International Workshop on Static Analysis”,
Padua, Italy,
September 1993.
 ILPS’93,
“International Logic Programming Symposium”, Vancouver,
British Columbia, Canada,
October 1993.
 AI*IA’93, “Terzo Congresso dell’Associazione Italiana per l’Intelligenza
Artificiale”, Torino, Italy,
October 1993.
 SAC’94, “ACM Symposium on Applied Computing”,
Phoenix, Arizona, USA,
March 1994
 ICLP’94, “International Conference on Logic Programming”,
S. Margherita Ligure, Italy,
June 1994.
 PLILP’94, “Programming Languages Implementation and Logic Programming”,
Madrid, Spain,
September 1994.
 ALP’94, “Third International Conference on Algebraic and Logic Programming”,
Madrid, Spain,
September 1994.
 GULPPRODE’94, “Joint Conference on Declarative Programming”,
Peñíscola, Spain,
September 1994.
 SAS’94, “International Static Analysis Symposium”,
Namur, Belgium,
September 1994.
 PLILP’95, “International Symposium on Programming Languages,
Implementations, Logics and Programs”,
Utrecht, Nederland,
September 1995.
 ILPS’95, “International Logic Programming Symposium”,
Portland, Oregon, USA,
December 1995.
 ESOP’96, “European Symposium on Programming”,
Linköping, Sweden,
April 1996.
 ECAI’96, “European Conference on Artificial Intelligence”
Budapest, Hungary,
August 1996.
 PLILP’96, “Eighth International Symposium on Programming Languages,
Implementations, Logics, and Programs”,
Aachen, Germany,
September 1996.
 SAS’96, “Third International Static Analysis Symposium”,
Aachen, Germany,
September 1996.
 LOPSTR’97, “Seventh International Workshop
on Logic Program Synthesis and Transformation”,
Leuven, Belgium,
July 1997.
 JICSLP’98, “Joint International Conference and Symposium
on Logic Programming”
Manchester, UK,
June 1998.
 SAS’98, “Fifth International Static Analysis Symposium”,
Pisa, Italy,
September 1998.
 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.
 SAS’99, “International Static Analysis Symposium”,
Venice, Italy,
September 1999.
 PPDP’99, “International Conference on Principles and Practice
of Declarative Programming”,
Paris, France,
September–October 1999.
 SAS 2000, “Seventh International Static Analysis Symposium”,
Santa Barbara, USA,
June–July 2000.
 ESSLLI2000,
“Twelfth European Summer School in Logic, Language and Information”,
student session,
Birmingham, UK,
August 2000.
 APPIAGULPPRODE’00,
“2000 Joint Conference on Declarative Programming”,
La Havana, Cuba,
December 2000.
 LPAR 2000,
“Seventh International Conference on Logic for
Programming and Automated Reasoning”,
Réunion Island, Indian Ocean, France,
November 2000.
 LPAR 2001,
“Eighth International Conference on Logic for
Programming, Artificial Intelligence and Reasoning”,
La Havana, Cuba,
December 2001.
 SAS’02, “Ninth International Static Analysis Symposium”,
Madrid, Spain,
September 2002.
 ESOP’03, “European Symposium on Programming”,
Warsaw, Poland,
April 2003.
 SAS’03, “Tenth International Static Analysis Symposium”,
San Diego, California, USA,
June 2003.
 PSI’03, “Perspectives of System Informatics”,
Novosibirsk, Akademgorodok, Russia,
July 2003.
 APPIAGULPPRODE’03,
“2003 Joint Conference on Declarative Programming”,
Reggio Calabria, Italy,
September 2003.
 WLPE’03,
“13th Workshop on Logic Programming Environments”,
Mumbai, India,
December 2003.
 VMCAI’04, “Fifth International Conference on Verification,
Model Checking and Abstract Interpretation”,
Venice, Italy,
January 2004.
 ESOP’04, “European Symposium on Programming”,
Barcelona, Spain,
March–April 2004.
 SAS’04, “Eleventh International Static Analysis Symposium”,
Verona, Italy,
August 2004.
 CAV’05,
“Seventeenth International Conference on Computer Aided Verification”,
The University of Edinburgh, Scotland, UK,
July 2005.
 SAS’05, “Twelfth International Static Analysis Symposium”,
London, UK,
September 2005.
 LOPSTR’05, “International Symposium on Logicbased Program
Synthesis and Transformation”,
London, UK,
September 2005.
 ICLP’05,
“Twenty First International Conference on Logic Programming”,
Barcelona, Spain,
October 2005.
 LOPSTR 2006,
“International Symposium on
Logicbased Program Synthesis and Transformation”,
S. Servolo, Venice, Italy,
July 2006.
 POPL 2007,
“Thirtyfourth Annual ACM SIGPLANSIGACT Symposium on
Principles of Programming Languages”,
Nice, France,
January 2007.
 ESOP’07,
“Sixteenth European Symposium on Programming”,
Braga, Portugal,
March, 2007.
 SAS 2007,
“Fourteenth International Static Analysis Symposium”,
Kongens Lyngby, Denmark,
August 2007.
 SAC 2008,
“Twentythird Annual ACM Symposium on Applied Computing”,
Technical Track on Software Verification,
Fortaleza, Ceará, Brasil,
March 2008.
 VMCAI 2008,
“Nineth International Conference on Verification, Model Checking,
and Abstract Interpretation”,
San Francisco, USA,
January 2008.
 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 Participant to the ESPRIT
Basic Research Action Project n. 6707, “ParForce”.
 Participant to the italian national project on
“Automatic Program Certification by Abstract Interpretation”
(1999–2001,
national coordinator: Prof. Roberto Giacobazzi, University of Verona).
 Participant to the italian national project on
“Abstract Interpretation, Type Systems and ControlFlow Analysis”
(2000–2002,
national coordinator: Prof. Giorgio Levi, University of Pisa).
 Coordinator for Italy of the bilateral project on
“Advanced Development Environments for Logic Programs”
(Azioni Integrate ItaliaSpagna 2001, code IT229,
2001–2003, coordinator for Spain:
Prof. Germán Puebla Sánchez, Facultad de Informática,
Universidad Politécnica de Madrid).
 Participant to the italian national project on
“Aggregate and NumberReasoning for Computing:
from Decision Algorithms to Constraint Programming with Multisets,
Sets, and Maps”
(2001–2003,
national coordinator: Prof. Domenico Cantone, University of Catania).
 Coordinator of the Parma research unit for the italian national project on
“ConstraintBased Verification of Reactive Systems”
(2002–2004,
national coordinator: Prof. Maurizio Gabbrielli, University of Bologna).
 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).
 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).
 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.
 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 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).
 Coordinator of the University of Parma research unit in the
ITEA2
(Information Technology for European Advancement)
project proposal
SAFEGCC (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 GaussSeidel
methods.
SIAM Review 37, 1 (1995), 93–97.
 [2]

Bagnara, R.
A hierarchy of constraint systems for dataflow analysis of
constraint logicbased languages.
Science of Computer Programming 30, 1–2 (1998), 119–155.
 [3]

Bagnara, R., Hill, P. M., and Zaffanella, E.
Setsharing is redundant for pairsharing.
Theoretical Computer Science 277, 12 (2002), 3–46.
 [4]

Hill, P. M., Bagnara, R., and Zaffanella, E.
Soundness, idempotence and commutativity of setsharing.
Theory and Practice of Logic Programming 2, 2 (2002), 155–201.
 [5]

Zaffanella, E., Hill, P. M., and Bagnara, R.
Decomposing nonredundant 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 setsharing, 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.
Finitetree analysis for constraint logicbased 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 constraintbased termination inference tool for
ISOProlog.
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.
Weaklyrelational 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., BernersLee, T. J., Carena, W., Divia, R.,
Parkman, C., Petersen, J., Tremblet, L., and Wessels, B.
The valetplus 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. (NorthHolland), Amsterdam, pp. 59–68.
 [20]

Heyes, G., Wessels, B., Perrin, Y., Bagnara, R., BernersLee, T. J.,
Carena, W., Divia, R., Parkman, C., Petersen, J., and Tremblet, L.
The integration of vax and valetplus data
acquisition software.
Contribution to the “Sixth Conference on RealTime 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 dataflow 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, SpringerVerlag, Berlin, pp. 107–121.
 [23]

Bagnara, R., Hill, P. M., and Zaffanella, E.
Setsharing is redundant for pairsharing.
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, SpringerVerlag, Berlin, pp. 53–67.
 [24]

Hill, P. M., Bagnara, R., and Zaffanella, E.
The correctness of setsharing.
In Static Analysis: Proceedings of the 5th International
Symposium (Pisa, Italy, 1998), G. Levi, Ed., vol. 1503 of Lecture
Notes in Computer Science, SpringerVerlag, Berlin, pp. 99–114.
 [25]

Bagnara, R., and Schachte, P.
Factorizing equivalent variable pairs in ROBDDbased
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, SpringerVerlag, 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, SpringerVerlag, Berlin, pp. 414–431.
 [27]

Zaffanella, E., Hill, P. M., and Bagnara, R.
Decomposing nonredundant 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, SpringerVerlag, 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, SpringerVerlag, Berlin, pp. 189–206.
 [30]

Bagnara, R., Gori, R., Hill, P. M., and Zaffanella, E.,
Finitetree analysis for constraint logicbased 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,
SpringerVerlag, Berlin, pp. 165–184.
 [31]

Bagnara, R., Zaffanella, E., Gori, R., and Hill, P. M.
Boolean functions for finitetree 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,
SpringerVerlag, 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, SpringerVerlag,
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, SpringerVerlag, 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, SpringerVerlag, Berlin, pp. 135–148.
 [35]

Bagnara, R., Hill, P. M., Mazzi, E., and Zaffanella, E.
Widening operators for weaklyrelational numeric abstractions.
In Static Analysis: Proceedings of the 12th International
Symposium (London, UK, 2005), C. Hankin, Ed., Lecture Notes in Computer
Science, SpringerVerlag, Berlin.
 [36]

Bagnara, R., RodríguezCarbonell, E., and Zaffanella, E.
Generation of basic semialgebraic invariants using convex polyhedra.
In Static Analysis: Proceedings of the 12th International
Symposium (London, UK, 2005), C. Hankin, Ed., Lecture Notes in Computer
Science, SpringerVerlag, 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 Logicbased Program Synthesis and Transformation, 16th
International Symposium (Venice, Italy, 2007), G. Puebla, Ed., vol. 4407
of Lecture Notes in Computer Science, SpringerVerlag, 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, SpringerVerlag, Berlin, pp. 8–21.
 [39]

Bagnara, R., Carlier, M., Gori, R., and Gotlieb, A.
Symbolic pathoriented test data generation for floatingpoint
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 (GULPPRODE’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 logicbased
languages.
In Proceedings of the “1995 Joint Conference on Declarative
Programming (GULPPRODE’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 (APPIAGULPPRODE’96)” (DonostiaSan 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 ANDcompositionality of CLP computed answer
constraints.
In Proceedings of the “1996 Joint Conference on Declarative
Programming (APPIAGULPPRODE’96)” (DonostiaSan 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 (APPIAGULPPRODE’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 (APPIAGULPPRODE’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 ROBDDbased
implementations of Pos.
In Proceedings of the “1998 Joint Conference on Declarative
Programming (APPIAGULPPRODE’98)” (A Coruña, Spain, 1998),
FreireNistal, J. L., Falaschi, M., and VilaresFerro, M., Eds.,
pp. 227–239.
 [48]

Hill, P. M., Bagnara, R., and Zaffanella, E.
The correctness of setsharing.
In Proceedings of the “1998 Joint Conference on Declarative
Programming (APPIAGULPPRODE’98)” (A Coruña, Spain, 1998),
FreireNistal, J. L., Falaschi, M., and VilaresFerro, M., Eds.,
pp. 255–267.
 [49]

Bagnara, R., Zaffanella, E., and Hill, P. M.
Enhancing Sharing for precision.
In Proceedings of the “APPIAGULPPRODE’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 “APPIAGULPPRODE’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 Componentbased
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 DSSETR20032, 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 Prologbased 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 “Logicbased 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) (AixenProvence, 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.
DataFlow Analysis for Constraint LogicBased Languages.
PhD thesis, Dipartimento di Informatica, Università di Pisa, Corso
Italia 40, I56125 Pisa, Italy, Mar. 1997.
Printed as Report TD1/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.
Setsharing is redundant for pairsharing.
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 setsharing.
Quaderno 188, Dipartimento di Matematica, Università di Parma,
1999.
 [61]

Zaffanella, E., Hill, P. M., and Bagnara, R.
Decomposing nonredundant 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.,
Finitetree analysis for constraint logicbased 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 finitetree 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 setsharing, 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 setsharing, 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.
Finitetree analysis for constraint logicbased 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 weaklyrelational 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.
Finitetree analysis for constraint logicbased 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íguezCarbonell, E., and Zaffanella, E.
Generation of basic semialgebraic invariants using convex polyhedra.
Report de recerca LSI0514R, 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.
InfoKermit Digest 6, 15 (July 1987).
 [86]

Bagnara, R.
A General Event Handling System for the ValetPlus.
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 SoftwareMost 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 PPLThe 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 nonclosed 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 memorybounded 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 exceptionsafe (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 uptodate 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 ECLAIRECLAIR 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 optionprocessing 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 httpd2.2.11.tar.bz2
$ cd httpd2.2.11
$ ./configure
$ eclair_env evalfile=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 nonsyntactic information.
(2)
As a number of interrelated C++ classes: a more complex
representation that, however, gives access to all the information.
The Prolog view makes it easy to code syntaxbased 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 semanticspreserving program transformer
that can simplify a program into a subset of C (or C++), the main
simplification consisting of the removal of sideeffects from
expressions. The simplified form, which is of course compilable and
semantically equivalent, makes it much easier to develop
semanticsbased program manipulations.
Coding Rule Checkers and Bug Finders
The coding rule checkers support the following rule sets:
MISRAC:2004, CERT C Secure Coding Standard,
JSF C++, HighIntegrity 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 fieldsensitive
pointer analysis along with numerical value analyses based on the
Parma Polyhedra Library, a stateoftheart 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 PURRSPurrs (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 CHINAChina (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 OCRAOcra (OccurCheck Reduction Analyzer) is a prototype
using the information provided by the China analyzer for the
occurcheck 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 occurcheck in the unification procedure.
5.8.6 CLAIRThe 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/.
[Page last updated on July 05, 2013, 17:06:08.]
