|
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 |
| 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 positionFull 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 writtenEnglish (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 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 1999-2000 and 2000-2001.
- “Laboratorio di informatica” (Laboratory of Computer Science),
degree in “Mathematics”,
academic year 2000-2001.
- “Programmazione (metodi avanzati)” (Advanced Programming Techniques),
degree in “Mathematics”,
academic years 2000-2001 and 2002-2003.
- “Programmazione 3” (3rd course on Programming),
degrees in “Mathematics” and “Mathematics and Computer Science”,
academic year 2002-2003.
- “Scrittura matematica e informatica”
(Writing for Mathematics and Computer Science),
degrees in “Mathematics” and “Mathematics and Computer Science”,
academic year 2002-2003.
- “Programmazione I” (1st course on Programming),
degrees in “Mathematics”,
“Mathematics and Computer Science”
e “Mathematics for Technology and Finance”,
academic year 2001-2002.
- “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.
- “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.
- “Scrittura matematica e informatica”
(Writing for Mathematics and Computer Science),
degree in “Computer Science”,
academic years 2003-2004, 2004-2005 and 2005-2006.
- “Linguaggi di programmazione”
(Programming Languages),
degree in “Computer Science”,
academic year 2006-2007, 2007-2008, 2008-2009, 2009-2010 and 2010-2011.
- “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.
- “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.
- “Algorithmique” (Algorithmics),
Licence de mathématiques,
Université de la Réunion,
academic year 2006-2007.
- “Laboratorio di informatica” (Laboratory of Computer Science),
Degree in “Environmental Sciences”,
University of Siena, Follonica (GR),
academic year 2007-2008.
-
“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.
- “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- 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.
- 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,
- 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.
- 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.
- 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-
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.
-
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.
-
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.
-
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.
-
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.
-
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.
-
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.
-
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.
-
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.
-
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.
-
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.
-
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.
-
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.
-
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.
-
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.
-
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- 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ó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.
-
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 high-school teachers of Mathematics organized by
the Faculty of Sciences of the University of Parma,
academic years 1997-1998 and 1998-1999.
- 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 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.
- 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, St 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 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.
- 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.
- “Data-Flow Analysis for Constraint Logic-Based 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 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.
- “Formal Methods: A Gentle Introduction”,
Atego/HighRely workshop on DO-178 & DO-254 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
Logic-based 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
Logic-based 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
Logic-based Program Synthesis and Transformation” (LOPSTR 2009),
Coimbra, Portugal, September 9–11, 2009.
- Scientific Committee member of
ArcheoFOSS 2010,
Foggia, Museo Civico, May 6-7, 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 PLILP-ALP’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
I-QMDAA 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.
- GULP-PRODE’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.
- ESSLLI-2000,
“Twelfth European Summer School in Logic, Language and Information”,
student session,
Birmingham, UK,
August 2000.
- APPIA-GULP-PRODE’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.
- APPIA-GULP-PRODE’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 Logic-based 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
Logic-based Program Synthesis and Transformation”,
S. Servolo, Venice, Italy,
July 2006.
- POPL 2007,
“Thirtyfourth Annual ACM SIGPLAN-SIGACT 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 Control-Flow 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 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).
- 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).
- 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).
- 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
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 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 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 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 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 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 (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 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.]
|