Home |
Personal Info |
Papers |
Teaching |
Links |
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 Floating-Point 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 Floating-Point 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. 229-238. 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) (Aix-en-Provence, France, 2013), pp. 11-20. Symbolic Path-Oriented Test Data Generation for Floating-Point 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. 47-67. 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. 889-927. |
| 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. 453-473.
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 |
| Published in 2009 |
Weakly-Relational 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. 279-323. 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. 4672-4691. 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, 1-2 (June 2008), pp. 3-21. 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. 8-21. 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. 75-80. Extended abstract. Published as Technical Report ICIS--R07015, 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 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 Logic-based Program Synthesis and Transformation (LOPSTR'06) (Venice, Italy, July 2006), volume 4407 of Lecture Notes in Computer Science, G. Puebla, Ed., pp. 219-235. 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. 449-466. |
| 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. 222-257. Precise Widening Operators for Convex Polyhedra, with Patricia M. Hill, Elisa Ricci, and Enea Zaffanella. Science of Computer Programming 58, 1-2 (October 2005), pp. 28-56. Widening Operators for Weakly-Relational 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. 3-18. Generation of Basic Semi-algebraic 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. 19-34. 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 Weakly-Relational 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. 1-43. cTI: a Constraint-Based Termination Inference Tool for ISO-Prolog, with Fred Mesnard. Theory and Practice of Logic Programming 5, 1&2 (January 2005), pp. 243-257. |
| Published in 2004 |
Widening Operators for Weakly-Relational 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
Finite-Tree Analysis for Constraint Logic-Based Languages, with Roberta Gori, Patricia M. Hill, and Enea Zaffanella. Information and Computation 193, 2 (September 2004), pp. 84-116. Finite-Tree Analysis for Constraint Logic-Based 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 Set-Sharing, 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. 289-323. 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. 135-148. 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. 337-354. 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. 213-229. A New Encoding of Not Necessarily Closed Convex Polyhedra, with Patricia M. Hill and Enea Zaffanella. In Proceedings of the 1st CoLogNet Workshop on Component-based 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. 147-153. 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. Set-Sharing is Redundant for Pair-Sharing, with Patricia M. Hill and Enea Zaffanella. Theoretical Computer Science 277, 1-2 (April 2002), pp. 3-46. Soundness, Idempotence and Commutativity of Set-Sharing, with Patricia M. Hill and Enea Zaffanella. Theory and Practice of Logic Programming 2, 2 (March 2002), pp. 155-201. Decomposing Non-Redundant Sharing by Complementation, with Enea Zaffanella and Patricia M. Hill. Theory and Practice of Logic Programming 2, 2 (March 2002), pp. 233-261. |
| Published in 2001 |
A Correct, Precise and Efficient Integration of Set-Sharing, 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 Finite-Tree 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. 579-594. Finite-Tree Analysis for Constraint Logic-Based 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. 165-184. Finite-Tree Analysis for Constraint Logic-Based 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 Finite-Tree 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. 103-114.
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. 189-206. 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 ROBDD-Based 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. 471-485.
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. 414-431. Decomposing Non-Redundant 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. 69-84. Enhancing Sharing for Precision, with Enea Zaffanella and Patricia M. Hill. In Proceedings of the "APPIA-GULP-PRODE'99 Joint Conference on Declarative Programming" (L'Aquila, Italy, September 1999), M. C. Meo and M. Vilares-Ferro, Eds., pp. 213-227. Widening Sharing, with Enea Zaffanella and Patricia M. Hill. In Proceedings of the "APPIA-GULP-PRODE'99 Joint Conference on Declarative Programming" (L'Aquila, Italy, September 1999), M. C. Meo and M. Vilares-Ferro, Eds., pp. 559-573. 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. 10-12. On the Quality of Available Prolog Implementations. The Association for Logic Programming Newsletter12, 2 (May 1999), pp. 12-14. |
| Published in 1998 |
A Hierarchy of Constraint Systems for Data-Flow Analysis of Constraint Logic-Based Languages.
Science of Computer Programming 30, 1-2 (January 1998),
pp. 119-155.
The Correctness of Set-Sharing, 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. 99-114. Factorizing Equivalent Variable Pairs in ROBDD-Based Implementations of Pos, with Peter Schachte. In Proceedings of the "1998 Joint Conference on Declarative Programming (APPIA-GULP-PRODE'98)" (A Coruña, Spain, July 1998), J. L. Freire-Nistal, M. Falaschi, and M. Vilares-Ferro, Eds., pp. 227-239. The Correctness of Set-Sharing, with Patricia M. Hill and Enea Zaffanella. In Proceedings of the "1998 Joint Conference on Declarative Programming (APPIA-GULP-PRODE'98)" (A Coruña, Spain, July 1998), J. L. Freire-Nistal, M. Falaschi, and M. Vilares-Ferro, Eds., pp. 255-267. |
| Published in 1997 |
Set-Sharing is Redundant for Pair-Sharing,
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. 53-67.
Structural Information Analysis for CLP Languages. In Proceedings of the "1997 Joint Conference on Declarative Programming (APPIA-GULP-PRODE'97)" (Grado, Italy, June 1997), M. Falaschi and M. Navarro and A. Policriti, Eds., pp. 81-92. Sharing Revisited, with Patricia M. Hill and Enea Zaffanella. In Proceedings of the "1997 Joint Conference on Declarative Programming (APPIA-GULP-PRODE'97)" (Grado, Italy, June 1997), M. Falaschi and M. Navarro and A. Policriti, Eds., pp. 69-80. Data-Flow Analysis for Constraint Logic-Based 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. 107-121.
Straight ROBDDS Are Not the Best for Pos. In Proceedings of the "1996 Joint Conference on Declarative Programming (APPIA-GULP-PRODE'96)" (Donostia-San Sebastían, Spain, July 1996), P. Lucio, M. Martelli, and M. Navarro, Eds., pp. 493-496. The AND-Compositionality of CLP Computed Answer Constraints, with Marco Comini, Francesca Scozzari, and Enea Zaffanella. In Proceedings of the "1996 Joint Conference on Declarative Programming (APPIA-GULP-PRODE'96)" (Donostia-San Sebastían, Spain, July 1996), P. Lucio, M. Martelli, and M. Navarro, Eds., pp. 355-366. |
| Published in 1995 |
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.
A Unified Proof for the Convergence of Jacobi and Gauss-Seidel Methods. SIAM Review 37, 1 (March 1995), pp. 93-97. |
| 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 (GULP-PRODE'94)" (Peñíscola, Spain, September 1994), M. Alpuente, R. Barbuti, and I. Ramos, Eds., pp. 312-326. |
| Published in 1993 | An Application of Constraint Propagation to Data-Flow 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. 270-276. |
| 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. 81-82 of Bigre, pp. 43-50. 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 General-Purpose Name Server. CERN Data Handling Division, Online Computing Group, September 1989. The Integration of VAX and Valet-Plus Data Acquisition Software, with G. Heyes, B. Wessels, Y. Perrin, T. J. Berners-Lee, W. Carena, R. Divia, C. Parkman, J. Petersen, and L. Tremblet. IEEE Transactions on Nuclear Science 36, 5 (May 1989), 1572-1576. Contribution to the "Sixth Conference on Real-Time Computer Applications in Nuclear, Particle, and Plasma Physics" (Williamsburg, VA, May 1989). The Valet-Plus Embedded into Large Physics Experiments, with Y. Perrin, T. J. Berners-Lee, 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. (North-Holland), Amsterdam, pp. 59-68. Remote Procedure Call. CERN Mini & Micro Computer Newsletter 20 (October 1988). A General Event Handling System for the Valet-Plus. CERN Data Handling Division, Online Computing Group, September 1988. Announcing Kermit68K, a Portable 68000 Kermit Program. Info-Kermit Digest 6, 15 (July 1987). |
[Page last updated on September 22, 2015, 08:18:40.]
bagnara@cs.unipr.it
Home | Personal | Papers | Teaching | Links