
Papers of Roberto Bagnara
Don't worry about people stealing your ideas.
If your ideas are any good,
you'll have to ram them down people's throats.
 Howard Aiken
This page contains references to almost everything
I have written and published, including some
old works that are mostly of historical interest.
The abstracts of the papers can be retrieved by clicking on their title.
From the abstract pages you can usually download the papers,
which are available in several formats.
The formats currently provided are:
gzipped DVI,
gzipped PostScript at 300, 600, and 1200 DPI resolutions,
and PDF.
Some writings are also available in HTML.
The correct BibTeX entries are always given.
A subset of the papers is listed in
dblp.


To Appear

Exploiting Binary FloatingPoint Representations for Constraint Propagation,
with Matthieu Carlier,
Roberta Gori,
and Arnaud Gotlieb.
To appear on the INFORMS Journal on Computing.

Published in 2015

Exploiting Binary FloatingPoint Representations for Constraint Propagation: The Complete Unabridged Version,
with Matthieu Carlier,
Roberta Gori,
and Arnaud Gotlieb.

Published in 2013

Eventual Linear Ranking Functions,
with Fred Mesnard.
In Proceedings of the 15th International Symposium on
Principles and Practice of Declarative Programming (PPDP 2013)
(Madrid, Spain, 2013), pp. 229238.
Détection des fonctions de rang linéaires à terme,
with Anthony Alezan,
Fred Mesnard, and
Étienne Payet.
In Actes des Neuvièmes Journées Francophones de Programmation par Contraintes (JFPC 2013) (AixenProvence, France, 2013),
pp. 1120.
Symbolic PathOriented Test Data Generation for FloatingPoint Programs,
with Matthieu Carlier,
Roberta Gori,
and Arnaud Gotlieb.
Proceedings of the Sixth IEEE International Conference
on Software Testing, Verification and Validation (ICST 2013)
(Luxembourg City, Luxembourg, 2013).

Published in 2012

The Automatic Synthesis of Linear Ranking Functions,
with Fred Mesnard,
Andrea Pescetti, and
Enea Zaffanella.
Information and Computation 215 (June 2012),
pp. 4767.
Coding Guidelines for Prolog,
with
Michael A. Covington,
Richard O'Keefe,
Jan Wielemaker, and
Simon Price.
Theory and Practice of Logic Programming 12, 6 (November 2012),
pp. 889927.

Published in 2010

Exact Join Detection for Convex Polyhedra and Other Numerical Abstractions,
with
Patricia M. Hill
and Enea Zaffanella.
Computational Geometry: Theory and Applications 43, 5
(July 2010), pp. 453473.
The Automatic Synthesis of Linear Ranking Functions: The Complete Unabridged Version (TR),
with Fred Mesnard,
Andrea Pescetti,
and Enea Zaffanella.
Technical Report.
Quaderno 498 (2010), Department of Mathematics, University of Parma, Italy.
Also published as preprint arXiv:cs.PL/1004.0944 available from
http://arxiv.org/.

Published in 2009

WeaklyRelational Shapes for Numeric Abstractions: Improved Algorithms and Proofs of Correctness,
with
Patricia M. Hill
and Enea Zaffanella.
Formal Methods in System Design 35, 3 (December 2009), pp. 279323.
Applications of Polyhedral Computations to the Analysis and Verification of Hardware and Software Systems,
with
Patricia M. Hill
and Enea Zaffanella.
Theoretical Computer Science 410, 46 (November 2009),
pp. 46724691.
Exact Join Detection for Convex Polyhedra and Other Numerical Abstractions (TR),
with Patricia M. Hill
and Enea Zaffanella.
Technical Report.
Quaderno 492 (2009), Department of Mathematics, University of Parma, Italy.

Published in 2008

The Parma Polyhedra Library: Toward a Complete Set of Numerical Abstractions for the Analysis and Verification of Hardware and Software Systems,
with
Patricia M. Hill
and Enea Zaffanella.
Science of Computer Programming 72, 12 (June 2008),
pp. 321.
An Improved Tight Closure Algorithm for Integer Octagonal Constraints,
with Patricia M. Hill
and Enea Zaffanella.
In Proceedings of the Nineth International Conference on Verification,
Model Checking and Abstract Interpretation (VMCAI 2008)
(San Francisco, USA, 2008),
vol. 4905 of Lecture Notes in Computer Science,
F. Logozzo, D. Peled, and L. Zuck, Eds., pp. 821.
On the Design of Generic Static Analyzers for Imperative Languages (TR),
with Patricia M. Hill,
Andrea Pescetti,
and Enea Zaffanella.
Technical Report.
Quaderno 485 (2008), Department of Mathematics, University of Parma, Italy.

Published in 2007

Verification of C Programs Via Natural Semantics and Abstract Interpretation,
with Patricia M. Hill,
Andrea Pescetti,
and Enea Zaffanella.
In Proceedings of the
IFM 2007
C/C++ Verification Workshop
(Oxford, UK, July 2007),
H. Tews, Ed., pp. 7580.
Extended abstract. Published as Technical Report ICISR07015,
Institute for Computing and Information Sciences (iCIS), Radboud University
Nijmegen, Nijmegen, The Netherlands.
An Improved Tight Closure Algorithm for Integer Octagonal Constraints (TR),
with Patricia M. Hill
and Enea Zaffanella.
Technical Report.
Quaderno 467 (2007), Department of Mathematics, University of Parma, Italy.
On the Design of Generic Static Analyzers for Modern Imperative Languages,
with Patricia M. Hill,
Andrea Pescetti,
and Enea Zaffanella.
Preprint arXiv:cs.PL/0703116 available from
http://arxiv.org/.
Grids: A Domain for Analyzing the Distribution of Numerical Values,
with
Katy Dobson,
Patricia M. Hill,
Matthew Mundell,
and Enea Zaffanella.
In Proceedings of the 16th International Symposium
on Logicbased Program Synthesis and Transformation (LOPSTR'06)
(Venice, Italy, July 2006),
volume 4407 of Lecture Notes in Computer Science,
G. Puebla, Ed., pp. 219235.
Applications of Polyhedral Computations to the Analysis and Verification of Hardware and Software Systems,
with Patricia M. Hill
and Enea Zaffanella.
Technical Report.
Quaderno 458 (2007), Department of Mathematics, University of Parma, Italy.

Published in 2006

The Parma Polyhedra Library: Toward a Complete Set of Numerical Abstractions for the Analysis and Verification of Hardware and Software Systems,
with Patricia M. Hill
and Enea Zaffanella.
Technical Report.
Quaderno 457 (2006), Department of Mathematics, University of Parma, Italy.
Widening Operators for Powerset Domains,
with
Patricia M. Hill
and Enea Zaffanella.
International Journal on Software Tools for Technology Transfer 8,
4/5 (August 2006),
pp. 449466.

Published in 2005

Not Necessarily Closed Convex Polyhedra and the Double Description Method,
with
Patricia M. Hill
and Enea Zaffanella.
Formal Aspects of Computing 17, 2 (August 2005),
pp. 222257.
Precise Widening Operators for Convex Polyhedra,
with
Patricia M. Hill,
Elisa Ricci,
and Enea Zaffanella.
Science of Computer Programming 58, 12 (October 2005),
pp. 2856.
Widening Operators for WeaklyRelational Numeric Abstractions,
with Patricia M. Hill,
Elena Mazzi,
and Enea Zaffanella.
In Proceedings of the 12th International Symposium
on Static Analysis (SAS'05)
(London, UK, September 2005),
vol. 3672 of Lecture Notes in Computer Science,
C. Hankin and I. Siveroni, Eds., pp. 318.
Generation of Basic Semialgebraic Invariants Using Convex Polyhedra,
with
Enric Rodríguez Carbonell
and Enea Zaffanella.
In Proceedings of the 12th International Symposium
on Static Analysis (SAS'05)
(London, UK, September 2005),
vol. 3672 of Lecture Notes in Computer Science,
C. Hankin and I. Siveroni, Eds., pp. 1934.
A Linear Domain for Analyzing the Distribution of Numerical Values,
with
Katy Dobson,
Patricia M. Hill,
Matthew Mundell,
and Enea Zaffanella.
Report 2005.06 (2005), School of Computing, University of Leeds, UK.
Widening Operators for WeaklyRelational Numeric Abstractions,
with Patricia M. Hill,
Elena Mazzi,
and Enea Zaffanella.
Technical Report.
Quaderno 399 (2005), Department of Mathematics, University of Parma, Italy.
Enhanced Sharing Analysis Techniques: A Comprehensive Evaluation,
with Patricia M. Hill
and Enea Zaffanella.
Theory and Practice of Logic Programming 5, 1&2 (January 2005),
pp. 143.
cTI: a ConstraintBased Termination Inference Tool for ISOProlog,
with Fred Mesnard.
Theory and Practice of Logic Programming 5, 1&2 (January 2005),
pp. 243257.

Published in 2004

Widening Operators for WeaklyRelational Numeric Abstractions,
with Patricia M. Hill,
Elena Mazzi,
and Enea Zaffanella.
Contribution to the International workshop on
"Numerical & Symbolic Abstract Domains"
(NSAD'05, Paris, January 21, 2005).
Extended abstract.
Also published as
arXiv:cs.PL/0412043 .
FiniteTree Analysis for Constraint LogicBased Languages,
with Roberta Gori,
Patricia M. Hill,
and Enea Zaffanella.
Information and Computation 193, 2 (September 2004),
pp. 84116.
FiniteTree Analysis for Constraint LogicBased Languages: The Complete Unabridged Version,
with Roberta Gori,
Patricia M. Hill,
and Enea Zaffanella.
Technical Report.
Quaderno 363 (2004), Department of Mathematics, University of Parma, Italy.
A Correct, Precise and Efficient Integration of SetSharing, Freeness and Linearity for the Analysis of Finite and Rational Tree Languages,
with Patricia M. Hill
and Enea Zaffanella.
Theory and Practice of Logic Programming 4, 3 (May 2004),
pp. 289323.
Widening Operators for Powerset Domains,
with Patricia M. Hill
and Enea Zaffanella.
Technical Report.
Quaderno 349 (2004), Department of Mathematics, University of Parma, Italy.
Checking and Bounding the Solutions of Some Recurrence Relations,
with
Alessandro Zaccagnini.
Technical Report.
Quaderno 344 (2004), Department of Mathematics, University of Parma, Italy.

Published in 2003

Widening Operators for Powerset Domains,
with Patricia M. Hill
and Enea Zaffanella.
In Proceedings of the Fifth International Conference on Verification,
Model Checking and Abstract Interpretation (VMCAI 2004)
(Venice, Italy, January 2004),
vol. 2937 of Lecture Notes in Computer Science,
B. Steffen and G. Levi, Eds., pp. 135148.
The Automatic Solution of Recurrence Relations. I. Linear Recurrences of Finite Order with Constant Coefficients,
with
Alessandro Zaccagnini
and Tatiana Zolo.
Technical Report.
Quaderno 334 (2003), Department of Mathematics, University of Parma, Italy.
Precise Widening Operators for Convex Polyhedra,
with Patricia M. Hill,
Elisa Ricci,
and Enea Zaffanella.
In Proceedings of the 10th International Symposium
on Static Analysis (SAS'03)
(San Diego, California, USA, June 2003),
vol. 2694 of Lecture Notes in Computer Science,
R. Cousot, Ed., pp. 337354.
Precise Widening Operators for Convex Polyhedra,
with
Patricia M. Hill,
Elisa Ricci,
and Enea Zaffanella.
Technical Report.
Quaderno 312 (2003), Department of Mathematics, University of Parma, Italy.

Published in 2002

A New Encoding and Implementation of Not Necessarily Closed Convex Polyhedra,
with
Patricia M. Hill
and Enea Zaffanella.
Technical Report.
Quaderno 305 (2002), Department of Mathematics, University of Parma, Italy.
Possibly Not Closed Convex Polyhedra and the Parma Polyhedra Library,
with Elisa Ricci,
Enea Zaffanella,
and Patricia M. Hill.
In Proceedings of the 9th International Symposium
on Static Analysis (SAS'02)
(Madrid, Spain, September 2002),
vol. 2477 of Lecture Notes in Computer Science,
M. V. Hermenegildo and G. Puebla, Eds., pp. 213229.
A New Encoding of Not Necessarily Closed Convex Polyhedra,
with Patricia M. Hill
and Enea Zaffanella.
In Proceedings of the 1st CoLogNet Workshop on Componentbased
Software Development and Implementation Technology
for Computational Logic Systems (ITCLS'02)
(Madrid, Spain, September 2002),
Published as TR Number CLIP4/02.0, Universidad Politécnica
de Madrid, Facultad de Informática,
M. Carro, C. Vacheret, and K.K. Lau, Eds., pp. 147153.
Possibly Not Closed Convex Polyhedra and the Parma Polyhedra Library,
with Elisa Ricci,
Patricia M. Hill,
and Enea Zaffanella.
Technical Report.
Quaderno 286 (2002), Department of Mathematics, University of Parma, Italy.
Foreign Language Interfaces for Prolog: A Terse Survey,
with Manuel Carro.
Technical Report.
Quaderno 283 (2002), Department of Mathematics, University of Parma, Italy.
SetSharing is Redundant for PairSharing,
with Patricia M. Hill
and Enea Zaffanella.
Theoretical Computer Science 277, 12 (April 2002),
pp. 346.
Soundness, Idempotence and Commutativity of SetSharing,
with Patricia M. Hill
and Enea Zaffanella.
Theory and Practice of Logic Programming 2, 2 (March 2002),
pp. 155201.
Decomposing NonRedundant Sharing by Complementation,
with Enea Zaffanella
and Patricia M. Hill.
Theory and Practice of Logic Programming 2, 2 (March 2002),
pp. 233261.

Published in 2001

A Correct, Precise and Efficient Integration of SetSharing, Freeness and Linearity for the Analysis of Finite and Rational Tree Languages,
with Patricia M. Hill
and Enea Zaffanella.
Technical Report.
Quaderno 273 (2001), Department of Mathematics, University of Parma, Italy.
Boolean Functions for FiniteTree Dependencies,
with Enea Zaffanella,
Roberta Gori,
and Patricia M. Hill.
In Proceedings of the 8th International Conference on
Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2001)
(Havana, Cuba, December 2001),
vol. 2250 of Lecture Notes in Computer Science,
R. Nieuwenhuis and A. Voronkov, Eds., pp. 579594.
FiniteTree Analysis for Constraint LogicBased Languages,
with Roberta Gori,
Patricia M. Hill,
and Enea Zaffanella.
In Proceedings of the 8th International Symposium
on Static Analysis (SAS'01)
(Paris, France, July 2001),
vol. 2126 of Lecture Notes in Computer Science,
P. Cousot, Ed., pp. 165184.
FiniteTree Analysis for Constraint LogicBased Languages,
with Roberta Gori,
Patricia M. Hill,
and Enea Zaffanella.
Technical Report.
Quaderno 251 (2001), Department of Mathematics, University of Parma, Italy.
Boolean Functions for FiniteTree Dependencies,
with Enea Zaffanella,
Roberta Gori,
and Patricia M. Hill.
Technical Report.
Quaderno 252 (2001), Department of Mathematics, University of Parma, Italy.

Published in 2000

Enhanced Sharing Analysis Techniques: A Comprehensive Evaluation,
with Enea Zaffanella
and Patricia M. Hill.
In Proceedings of the 2nd International ACM SIGPLAN Conference
on Principles and Practice of Declarative Programming
(PPDP'00)"
(Montreal, Canada, September 2000),
ACM Press,
M. Gabbrielli and F. Pfenning, Eds., pp. 103114.
Efficient Structural Information Analysis for Real CLP Languages,
with Patricia M. Hill
and Enea Zaffanella.
In Proceedings of the "7th International Conference on
Logic for Programming and Automated Reasoning (LPAR'2000)"
(Reunion Island, France, November 2000),
vol. 1955 of Lecture Notes in Artificial Intelligence,
M. Parigot and A. Voronkov, Eds., pp. 189206.
Efficient Structural Information Analysis for Real CLP Languages,
with Patricia M. Hill
and Enea Zaffanella.
Technical Report.
Quaderno 229 (2000), Department of Mathematics, University of Parma, Italy.

Published in 1999

Factorizing Equivalent Variable Pairs in ROBDDBased Implementations of Pos,
with Peter Schachte.
In Proceedings of the
"Seventh International Conference on
Algebraic Methodology and Software Technology
(AMAST'98)"
(Amazonia, Brazil, January 1999),
vol. 1548 of Lecture Notes in Computer Science,
A. M. Haeberer, Ed., pp. 471485.
Widening Sharing,
with Patricia M. Hill and Enea Zaffanella.
In Proceedings of the 1st International Conference
on Principles and Practice of Declarative Programming (PPDP'99)
(Paris, France, September/October 1999),
vol. 1702 of Lecture Notes in Computer Science,
G. Nadathur, Ed., pp. 414431.
Decomposing NonRedundant Sharing by Complementation,
with Patricia M. Hill and Enea Zaffanella.
In Proceedings of the 6th International Symposium
on Static Analysis (SAS'99)
(Venice, Italy, September 1999),
vol. 1694 of Lecture Notes in Computer Science,
A. Cortesi and G. Filé, Eds., pp. 6984.
Enhancing Sharing for Precision,
with Enea Zaffanella
and Patricia M. Hill.
In Proceedings of the "APPIAGULPPRODE'99 Joint Conference on Declarative Programming"
(L'Aquila, Italy, September 1999),
M. C. Meo and M. VilaresFerro, Eds., pp. 213227.
Widening Sharing,
with Enea Zaffanella
and Patricia M. Hill.
In Proceedings of the "APPIAGULPPRODE'99 Joint Conference on Declarative Programming"
(L'Aquila, Italy, September 1999),
M. C. Meo and M. VilaresFerro, Eds., pp. 559573.
Precise and Practical Mode Analysis with the Analyzer.
Computational Logic:
The Newsletter of the
European Network in Computational Logic 7, (November 1999).
Is the ISO Prolog Standard Taken Seriously?
The Association for Logic Programming Newsletter12, 1 (February 1999),
pp. 1012.
On the Quality of Available Prolog Implementations.
The Association for Logic Programming Newsletter12, 2 (May 1999),
pp. 1214.

Published in 1998

A Hierarchy of Constraint Systems for DataFlow Analysis of Constraint LogicBased Languages.
Science of Computer Programming 30, 12 (January 1998),
pp. 119155.
The Correctness of SetSharing,
with Patricia M. Hill and Enea Zaffanella.
In Proceedings of the 5th International Symposium on Static Analysis (SAS'98)
(Pisa, Italy, September 1998), vol. 1503 of Lecture Notes in Computer Science,
G. Levi, Ed., pp. 99114.
Factorizing Equivalent Variable Pairs in ROBDDBased Implementations of Pos,
with Peter Schachte.
In Proceedings of the "1998 Joint Conference on Declarative
Programming (APPIAGULPPRODE'98)"
(A Coruña, Spain, July 1998),
J. L. FreireNistal, M. Falaschi, and M. VilaresFerro, Eds., pp. 227239.
The Correctness of SetSharing,
with Patricia M. Hill and Enea Zaffanella.
In Proceedings of the "1998 Joint Conference on Declarative
Programming (APPIAGULPPRODE'98)"
(A Coruña, Spain, July 1998),
J. L. FreireNistal, M. Falaschi, and M. VilaresFerro, Eds., pp. 255267.

Published in 1997

SetSharing is Redundant for PairSharing,
with Patricia M. Hill and Enea Zaffanella.
In Proceedings of the 4th International Symposium on Static Analysis (SAS'97)
(Paris, France, September 1997), vol. 1302 of Lecture Notes in Computer Science,
P. Van Hentenryck, Ed., pp. 5367.
Structural Information Analysis for CLP Languages.
In Proceedings of the "1997 Joint Conference on Declarative
Programming (APPIAGULPPRODE'97)"
(Grado, Italy, June 1997),
M. Falaschi and M. Navarro and A. Policriti, Eds., pp. 8192.
Sharing Revisited,
with Patricia M. Hill and Enea Zaffanella.
In Proceedings of the "1997 Joint Conference on Declarative
Programming (APPIAGULPPRODE'97)"
(Grado, Italy, June 1997),
M. Falaschi and M. Navarro and A. Policriti, Eds., pp. 6980.
DataFlow Analysis for Constraint LogicBased Languages.
Ph.D. dissertation, University of Pisa, March 1997.

Published in 1996

A Reactive Implementation of Pos Using ROBDDs.
In Proceedings of the "Eighth International Symposium on Programming
Languages, Implementations, Logics, and Programs (PLILP'96)"
(Aachen, Germany, September 1996), vol. 1140 of Lecture Notes in Computer Science,
H. Kuchen and S. D. Swierstra, Eds., pp. 107121.
Straight ROBDDS Are Not the Best for Pos.
In Proceedings of the "1996 Joint Conference on Declarative
Programming (APPIAGULPPRODE'96)"
(DonostiaSan Sebastían, Spain, July 1996),
P. Lucio, M. Martelli, and M. Navarro, Eds., pp. 493496.
The ANDCompositionality of CLP Computed Answer Constraints,
with Marco Comini, Francesca Scozzari, and Enea Zaffanella.
In Proceedings of the "1996 Joint Conference on Declarative
Programming (APPIAGULPPRODE'96)"
(DonostiaSan Sebastían, Spain, July 1996),
P. Lucio, M. Martelli, and M. Navarro, Eds., pp. 355366.

Published in 1995

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. 581592.
A Unified Proof for the Convergence of Jacobi and GaussSeidel Methods.
SIAM Review 37, 1 (March 1995), pp. 9397.

Published in 1994

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

Published in 1993

An Application of Constraint Propagation to DataFlow Analysis,
with Roberto Giacobazzi
and Giorgio Levi.
In Proceedings of "The Ninth Conference on Artificial Intelligence
for Applications" (Orlando, Florida, March 1993),
IEEE Computer Society Press, Los Alamitos, CA, pp. 270276.

Published in 1992

Static Analysis of CLP Programs over Numeric Domains,
with Roberto Giacobazzi and Giorgio Levi.
In Actes "Workshop on Static Analysis" (WSA'92, Bordeaux, September 1992),
M. Billaud, P. Castéran, M. Corsini, K. Musumbu, and
A. Rauzy, Eds., vol. 8182 of Bigre, pp. 4350.
Extended abstract.

Old Works

Interpretazione Astratta di Linguaggi Logici con Vincoli su Domini Finiti.
M.Sc. dissertation, University of Pisa, July 1992.
In Italian.
WAY (Where Are You?): A Simple GeneralPurpose Name Server.
CERN Data Handling Division, Online Computing Group, September 1989.
The Integration of VAX and ValetPlus Data Acquisition Software,
with G. Heyes, B. Wessels, Y. Perrin,
T. J. BernersLee,
W. Carena, R. Divia, C. Parkman, J. Petersen, and L. Tremblet.
IEEE Transactions on Nuclear Science 36, 5 (May 1989),
15721576.
Contribution to the "Sixth Conference on RealTime Computer
Applications in Nuclear, Particle, and Plasma Physics" (Williamsburg, VA,
May 1989).
The ValetPlus Embedded into Large Physics Experiments,
with Y. Perrin,
T. J. BernersLee, W. Carena, R. Divia,
C. Parkman, J. Petersen, L. Tremblet, and B. Wessels.
In Proceedings of the "VMEbus in Research International Conference"
(Zürich, October 1988), C. Eck and C. Parkman, Eds.,
Elsevier Science Publishers B.V. (NorthHolland),
Amsterdam, pp. 5968.
Remote Procedure Call.
CERN Mini & Micro Computer Newsletter 20 (October 1988).
A General Event Handling System for the ValetPlus.
CERN Data Handling Division, Online Computing Group, September 1988.
Announcing Kermit68K, a Portable 68000 Kermit Program.
InfoKermit Digest 6, 15 (July 1987).

[Page last updated on September 22, 2015, 08:18:40.]
