
Papers of Enea Zaffanella
[Page last updated on "aprile 16, 2018, 18:44:22".]


[ToAppear]
~~~
[2010201x]
~~~
[20052009]
~~~
[20002004]
~~~
[19941999]

To appear

A Direct Encoding for NNC Polyhedra.
Anna Becchi and Enea Zaffanella.
To appear in Proceedings of the 30th International Conference on Computer Aided Verification (CAV 2018) (Oxford, UK, July 2018).

[ToAppear]
~~~
[2010201x]
~~~
[20052009]
~~~
[20002004]
~~~
[19941999]

Published in 2018

On the Efficiency of Convex Polyhedra.
Enea Zaffanella.
Electronic Notes in Theoretical Computer Science.

Published in 2017

A Conversion Procedure for NNC Polyhedra.
Anna Becchi and Enea Zaffanella.
Preprint arXiv:1711.09593 available from
http://arxiv.org/.

Published in 2014

Efficient Constraint/Generator Removal
from Double Description of Polyhedra.
Gianluca Amato, Francesca Scozzari and Enea Zaffanella.
Electronic Notes in Theoretical Computer Science.

Published in 2012

A new look at the automatic synthesis of linear ranking functions.
Roberto Bagnara, Fred Mesnard, Andrea Pescetti and Enea Zaffanella.
Information and Computation.

Published in 2010

Exact Join Detection for Convex Polyhedra
and Other Numerical Abstractions.
Roberto Bagnara, Patricia M. Hill, and Enea Zaffanella.
Computational Geometry: Theory and Applications.
The Automatic Synthesis of Linear Ranking Functions:
The Complete Unabridged Version.
Roberto Bagnara, Fred Mesnard, Andrea Pescetti and Enea Zaffanella.
Technical Report.
Quaderno 498 (2010), Department of Mathematics, University of Parma, Italy.

[ToAppear]
~~~
[2010201x]
~~~
[20052009]
~~~
[20002004]
~~~
[19941999]

Published in 2009

WeaklyRelational Shapes for Numeric Abstractions: Improved Algorithms
and Proofs of Correctness.
Roberto Bagnara, Patricia M. Hill, and Enea Zaffanella.
Formal Methods in System Design.
Applications of Polyhedral Computations to the Analysis and Verification
of Hardware and Software Systems.
Roberto Bagnara, Patricia M. Hill, and Enea Zaffanella.
Theoretical Computer Science.
Exact Join Detection for Convex Polyhedra
and Other Numerical Abstractions.
Roberto Bagnara, 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.
Roberto Bagnara, Patricia M. Hill, and Enea Zaffanella.
Science of Computer Programming.
An Improved Tight Closure Algorithm for Integer Octagonal Constraints.
Roberto Bagnara, Patricia M. Hill, and Enea Zaffanella.
In
Proceedings of the 9th International Conference on
Verification, Model Checking and Abstract Interpretation
(VMCAI'08), (San Francisco, USA, January 2008),
vol. 4905 of Lecture Notes in Computer Science,
F. Logozzo and D. Peled and L. D. Zuck, Eds., pp. 821.
On the Design of Generic Static Analyzers for Imperative Languages.
Roberto Bagnara, 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.
Roberto Bagnara, 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.
Roberto Bagnara, 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.
Roberto Bagnara, Andrea Pescetti, Patricia M. Hill, and Enea Zaffanella.
Preprint arXiv:cs.PL/0703116 available from
http://arxiv.org/
Grids: A Domain for Analyzing the Distribution of Numerical Values.
Roberto Bagnara, 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.
Roberto Bagnara, 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.
Roberto Bagnara, Patricia M. Hill, and Enea Zaffanella.
Technical Report.
Quaderno 457 (2006), Department of Mathematics, University of Parma, Italy.
Widening Operators for Powerset Domains.
Roberto Bagnara, Patricia M. Hill, and Enea Zaffanella.
International Journal on Software Tools for Technology Transfer.

Published in 2005

A linear domain for analyzing the distribution of numerical values.
Roberto Bagnara, Katy Dobson, Patricia M. Hill, Matthew Mundell, and Enea Zaffanella.
Report 2005.06, School of Computing, University of Leeds, UK, 2005.
PURRS: Towards computer algebra support for fully automatic worstcase
complexity analysis.
Roberto Bagnara, Andrea Pescetti, Alessandro Zaccagnini, and Enea Zaffanella.
Published as
arXiv:cs.MS/0512056.
Widening Operators for WeaklyRelational Numeric Abstractions.
Roberto Bagnara, Patricia M. Hill, Elena Mazzi, and Enea Zaffanella.
In Proceedings of the 12th International Symposium on Static
Analysis (SAS'05) (London, UK, September 2005),
volume 3672 of Lecture Notes in Computer Science,
C. Hankin and I. Siveroni, Eds., pp. 318.
Generation of Basic Semialgebraic Invariants Using Convex Polyhedra.
Roberto Bagnara, Enric RodríguezCarbonell, and Enea Zaffanella.
In Proceedings of the 12th International Symposium on Static
Analysis (SAS'05) (London, UK, September 2005),
volume 3672 of Lecture Notes in Computer Science,
C. Hankin and I. Siveroni, Eds., pp. 1934.
Precise Widening Operators for Convex Polyhedra.
Roberto Bagnara, Patricia M. Hill, Elisa Ricci, and Enea Zaffanella.
Science of Computer Programming.
Not Necessarily Closed Convex Polyhedra and
the Double Description Method.
Roberto Bagnara, Patricia M. Hill, and Enea Zaffanella.
Formal Aspects of Computing.
Generation of basic semialgebraic invariants using convex polyhedra.
Roberto Bagnara, Enric RodríguezCarbonell, and Enea Zaffanella.
Report de recerca LSI0514R, Departament de Llenguatges i Sistemes
Informàtics, Universitat Politècnica de Catalunya,
Barcelona, Spain, 2005.
Widening Operators for WeaklyRelational Numeric Abstractions.
Roberto Bagnara, 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.
Roberto Bagnara, Enea Zaffanella, and Patricia M. Hill.
Theory and Practice of Logic Programming.

[ToAppear]
~~~
[2010201x]
~~~
[20052009]
~~~
[20002004]
~~~
[19941999]

Published in 2004

Widening Operators for WeaklyRelational Numeric Abstractions.
Roberto Bagnara, 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.
Roberto Bagnara, Roberta Gori, Patricia M. Hill, and Enea Zaffanella.
Information and Computation.
FiniteTree Analysis for Constraint LogicBased Languages:
The Complete Unabridged Version.
Roberto Bagnara, 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.
Patricia M. Hill, Enea Zaffanella, and Roberto Bagnara.
Theory and Practice of Logic Programming.
Widening Operators for Powerset Domains.
Roberto Bagnara, Patricia M. Hill, and Enea Zaffanella.
Technical Report.
Quaderno 349 (2004), Department of Mathematics, University of Parma, Italy.

Published in 2003

Widening Operators for Powerset Domains.
Roberto Bagnara, Patricia M. Hill, and Enea Zaffanella.
In
Proceedings of the 5th International Conference on
Verification, Model Checking and Abstract Interpretation
(VMCAI'04), (Venezia, Italy, January 2004),
vol. 2937 of Lecture Notes in Computer Science,
B. Steffen and G. Levi, Eds., pp. 135148.
Precise Widening Operators for Convex Polyhedra.
Roberto Bagnara, Patricia M. Hill, Elisa Ricci, and Enea Zaffanella.
In Proceedings of the 10th International Static Analysis Symposium
(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.
Roberto Bagnara, 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.
Roberto Bagnara, 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.
Roberto Bagnara, 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.
Roberto Bagnara, 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.
Roberto Bagnara, Elisa Ricci, Enea Zaffanella, and Patricia M. Hill.
Technical Report.
Quaderno 286 (2002), Department of Mathematics, University of Parma, Italy.
Setsharing is redundant for pairsharing.
Roberto Bagnara, Patricia M. Hill, and Enea Zaffanella.
Theoretical Computer Science.
Soundness, Idempotence and Commutativity of SetSharing.
Patricia M. Hill, Roberto Bagnara, and Enea Zaffanella.
Theory and Practice of Logic Programming.
Decomposing NonRedundant Sharing by Complementation.
Enea Zaffanella, Patricia M. Hill, and Roberto Bagnara.
Theory and Practice of Logic Programming.

Published in 2001

A Correct, Precise and Efficient Integration
of SetSharing, Freeness and Linearity
for the Analysis of Finite and Rational Tree Languages.
Patricia M. Hill, Enea Zaffanella, and Roberto Bagnara.
Technical Report.
Quaderno 273 (2001), Department of Mathematics, University of Parma, Italy.
Boolean Functions for FiniteTree Dependencies.
Roberto Bagnara, 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 Artificial Intelligence,
R. Nieuwenhuis and A. Voronkov, Eds., pp. 575589.
Correctness, Precision and Efficiency
in the Sharing Analysis of Real Logic Languages.
Enea Zaffanella.
PhD thesis  School of Computing of
the University of Leeds, September 2001.
FiniteTree Analysis for Constraint LogicBased Languages.
Roberto Bagnara, Roberta Gori, Patricia M. Hill, and Enea Zaffanella.
In Proceedings of the 8th International Symposium
on Static Analysys (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.
Roberto Bagnara, 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.
Roberto Bagnara, Enea Zaffanella, Roberta Gori, and Patricia M. Hill.
Technical Report.
Quaderno 252 (2001), Department of Mathematics, University of Parma, Italy.

Published in 2000

Efficient Structural Information Analysis for Real CLP Languages.
Roberto Bagnara, 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.
Enhanced Sharing Analysis Techniques: A Comprehensive Evaluation.
Roberto Bagnara, 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), M. Gabbrielli and F. Pfenning, Eds.,
pp. 103114. ACM Press, New York.
Efficient Structural Information Analysis for Real CLP Languages.
Roberto Bagnara, Patricia M. Hill, and Enea Zaffanella.
Technical Report.
Quaderno 229, Department of Mathematics, University of Parma, Italy.

[ToAppear]
~~~
[2010201x]
~~~
[20052009]
~~~
[20002004]
~~~
[19941999]

Published in 1999

Widening Sharing.
Enea Zaffanella, Roberto Bagnara, and Patricia M. Hill.
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.
Enea Zaffanella, Patricia M. Hill, and Roberto Bagnara.
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.
Roberto Bagnara, 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.
Enea Zaffanella, Roberto Bagnara, 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.

Published in 1998

The correctness of setsharing.
Patricia M. Hill, Roberto Bagnara, 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.
The correctness of setsharing.
Patricia M. Hill, Roberto Bagnara, 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

Abstracting Synchronization in Concurrent Constraint Programming.
Enea Zaffanella, Roberto Giacobazzi, and Giorgio Levi.
The Journal of Functional and Logic Programming.
Setsharing is redundant for pairsharing.
Roberto Bagnara, 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.
Sharing revisited.
Roberto Bagnara, 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.

Published in 1996

Modular Analysis of Suspension Free cc Programs.
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.
The ANDcompositionality of CLP computed answer constraints.
Roberto Bagnara, 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

Domain Independent Ask Approximation in CCP.
Enea Zaffanella.
In Proceedings of the ``First International Conference on ``Principles
and Practice of Constraint Programming (CP'95)''
(Cassis, France, September 1995),
vol. 976 of Lecture Notes in Computer Science,
U. Montanari and F. Rossi, Eds., pp. 362379.
Domain Independent Ask Approximation in CCP.
Enea Zaffanella.
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. 89100.

Published in 1994

Abstracting Synchronization in Concurrent Constraint Programming.
Enea Zaffanella, Roberto Giacobazzi, and Giorgio Levi.
In Proceedings of the Sixth International Symposium on ``Programming
Language Implementation and Logic Programming (PLILP'94)''
(Madrid, Spain, September 1994),
vol. 844 of Lecture Notes in Computer Science,
M. Hermenegildo and J. Penjam, Eds., pp. 5772.

[ToAppear]
~~~
[2010201x]
~~~
[20052009]
~~~
[20002004]
~~~
[19941999]

