
Papers of Enea Zaffanella
[Page last updated on "settembre 26, 2020, 09:16:10".]


[ToAppear]
~~~
[2020202x]
~~~
[20152019]
~~~
[20102014]
~~~
[20052009]
~~~
[20002004]
~~~
[19941999]

To appear

PPLite: ZeroOverhead Encoding of NNC Polyhedra.
A. Becchi, E. Zaffanella.
Information and Computation.

[ToAppear]
~~~
[2020202x]
~~~
[20152019]
~~~
[20102014]
~~~
[20052009]
~~~
[20002004]
~~~
[19941999]

Published in 2020

Synthesis of Pstable Abstractions.
A. Becchi, A. Cimatti, E. Zaffanella.
Software Engineering and Formal Methods 2020 (SEFM 2020)
(Amsterdam, The Netherlands, September 2020).
ARCHCOMP20 Category Report:
Hybrid Systems with Piecewise Constant Dynamics and Bounded Model Cheking.
L. Bu, A. Abate, D. Adzkiya, M.S. Mufid, R. Ray, Y. Wu, E. Zaffanella.
7th International Workshop on Applied Verification
of Continuous and Hybrid Systems (ARCH20) (Berlin, Germany, July 2020).

[ToAppear]
~~~
[2020202x]
~~~
[20152019]
~~~
[20102014]
~~~
[20052009]
~~~
[20002004]
~~~
[19941999]

Published in 2019

Revisiting Polyhedral Analysis for Hybrid Systems.
A. Becchi, E. Zaffanella.
Static Analysis  26th International Symposium (SAS 2019)
(Porto, Portugal, October 2019).
A. Becchi received the
Radhia Cousot Young Researcher Best Paper Award.
Some thoughts on the design of abstract domains.
E. Zaffanella.
Invited talk at the
8th International Workshop on Numerical and Symbolic Abstract Domains
(NSAD 2019)
(Porto, Portugal, October 2019).
ARCHCOMP19 Category Report:
Hybrid Systems with Piecewise Constant Dynamics.
G. Frehse, A. Abate, D. Adzkiya, A. Becchi,
L. Bu, A. Cimatti, M. Giacobbe, A. Griggio,
S. Mover, M.S. Mufid, I. Riouak, S. Tonetta,
E. Zaffanella.
6th International Workshop on Applied Verification
of Continuous and Hybrid Systems (ARCH19) (Montreal, Canada, April 2019).

Published in 2018

An Efficient Abstract Domain for Not Necessarily Closed Polyhedra.
A. Becchi, E. Zaffanella.
Static Analysis  25th International Symposium (SAS 2018) (Freiburg, Germany, August 2018).
A Direct Encoding for NNC Polyhedra.
A. Becchi, E. Zaffanella.
Proceedings of the 30th International Conference on Computer Aided Verification (CAV 2018) (Oxford, UK, July 2018).
ARCHCOMP18 Category Report:
Hybrid Systems with Piecewise Constant Dynamics.
G. Frehse, A. Abate, D. Adzkiya, L. Bu, M. Giacobbe,
M.S. Mufid, E. Zaffanella.
5th International Workshop on Applied Verification
of Continuous and Hybrid Systems (ARCH18) (Oxford, UK, July 2018).
On the Efficiency of Convex Polyhedra.
E. Zaffanella.
Electronic Notes in Theoretical Computer Science.

Published in 2017

A Conversion Procedure for NNC Polyhedra.
A. Becchi, E. Zaffanella.
Preprint arXiv:1711.09593 .

[ToAppear]
~~~
[2020202x]
~~~
[20152019]
~~~
[20102014]
~~~
[20052009]
~~~
[20002004]
~~~
[19941999]

Published in 2014

Efficient Constraint/Generator Removal
from Double Description of Polyhedra.
G. Amato, F. Scozzari, E. Zaffanella.
Electronic Notes in Theoretical Computer Science.

Published in 2012

A new look at the automatic synthesis of linear ranking functions.
R. Bagnara, F. Mesnard, A. Pescetti, E. Zaffanella.
Information and Computation.

Published in 2010

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

[ToAppear]
~~~
[2020202x]
~~~
[20152019]
~~~
[20102014]
~~~
[20052009]
~~~
[20002004]
~~~
[19941999]

Published in 2009

WeaklyRelational Shapes for Numeric Abstractions: Improved Algorithms
and Proofs of Correctness.
R. Bagnara, P.M. Hill, E. Zaffanella.
Formal Methods in System Design.
Applications of Polyhedral Computations to the Analysis and Verification
of Hardware and Software Systems.
R. Bagnara, P.M. Hill, E. Zaffanella.
Theoretical Computer Science.
Exact Join Detection for Convex Polyhedra
and Other Numerical Abstractions.
R. Bagnara, P.M. Hill, E. 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.
R. Bagnara, P.M. Hill, E. Zaffanella.
Science of Computer Programming.
An Improved Tight Closure Algorithm for Integer Octagonal Constraints.
R. Bagnara, P.M. Hill, E. Zaffanella.
9th International Conference on
Verification, Model Checking and Abstract Interpretation (VMCAI'08),
(San Francisco, USA, January 2008).
On the Design of Generic Static Analyzers for Imperative Languages.
R. Bagnara, P.M. Hill, A. Pescetti, E. 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.
R. Bagnara, P.M. Hill, A. Pescetti, E. Zaffanella.
IFM 2007 C/C++ Verification Workshop (Oxford, UK, July 2007),
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.
R. Bagnara, P.M. Hill, E. Zaffanella.
Technical Report.
Quaderno 467 (2007), Department of Mathematics, University of Parma, Italy.
On the Design of Generic Static Analyzers
for Modern Imperative Languages.
R. Bagnara, A. Pescetti, P.M. Hill, E. Zaffanella.
Preprint arXiv:cs.PL/0703116 available from
http://arxiv.org/
Grids: A Domain for Analyzing the Distribution of Numerical Values.
R. Bagnara, K. Dobson, P.M. Hill, M. Mundell, E. Zaffanella.
16th International Symposium on Logicbased
Program Synthesis and Transformation (LOPSTR'06)
(Venice, Italy, July 2006).
Applications of Polyhedral Computations to the Analysis and Verification
of Hardware and Software Systems.
R. Bagnara, P.M. Hill, E. 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.
R. Bagnara, P.M. Hill, E. Zaffanella.
Technical Report.
Quaderno 457 (2006), Department of Mathematics, University of Parma, Italy.
Widening Operators for Powerset Domains.
R. Bagnara, P.M. Hill, E. Zaffanella.
International Journal on Software Tools for Technology Transfer.

Published in 2005

A linear domain for analyzing the distribution of numerical values.
R. Bagnara, K. Dobson, P.M. Hill, M. Mundell, E. Zaffanella.
Report 2005.06, School of Computing, University of Leeds, UK, 2005.
PURRS: Towards computer algebra support for fully automatic worstcase
complexity analysis.
R. Bagnara, A. Pescetti, A. Zaccagnini, E. Zaffanella.
Published as
arXiv:cs.MS/0512056.
Widening Operators for WeaklyRelational Numeric Abstractions.
R. Bagnara, P.M. Hill, E. Mazzi, E. Zaffanella.
12th International Symposium on Static Analysis (SAS'05)
(London, UK, September 2005).
Generation of Basic Semialgebraic Invariants Using Convex Polyhedra.
R. Bagnara, E. RodríguezCarbonell, E. Zaffanella.
12th International Symposium on Static Analysis (SAS'05)
(London, UK, September 2005).
Precise Widening Operators for Convex Polyhedra.
R. Bagnara, P.M. Hill, E. Ricci, E. Zaffanella.
Science of Computer Programming.
Not Necessarily Closed Convex Polyhedra and
the Double Description Method.
R. Bagnara, P.M. Hill, E. Zaffanella.
Formal Aspects of Computing.
Generation of basic semialgebraic invariants using convex polyhedra.
R. Bagnara, E. RodríguezCarbonell, E. 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.
R. Bagnara, P.M. Hill, E. Mazzi, E. Zaffanella.
Technical Report.
Quaderno 399 (2005), Department of Mathematics, University of Parma, Italy.
Enhanced Sharing Analysis Techniques: a Comprehensive Evaluation.
R. Bagnara, E. Zaffanella, P.M. Hill.
Theory and Practice of Logic Programming.

[ToAppear]
~~~
[2020202x]
~~~
[20152019]
~~~
[20102014]
~~~
[20052009]
~~~
[20002004]
~~~
[19941999]

Published in 2004

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

Published in 2003

Widening Operators for Powerset Domains.
R. Bagnara, P.M. Hill, E. Zaffanella.
5th International Conference on
Verification, Model Checking and Abstract Interpretation (VMCAI'04),
(Venezia, Italy, January 2004).
Precise Widening Operators for Convex Polyhedra.
R. Bagnara, P.M. Hill, E. Ricci, E. Zaffanella.
10th International Static Analysis Symposium (SAS'03),
(San Diego, California, USA, June 2003).
Precise Widening Operators for Convex Polyhedra.
R. Bagnara, P.M. Hill, E. Ricci, E. 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.
R. Bagnara, P.M. Hill, E. Zaffanella.
Technical Report.
Quaderno 305 (2002), Department of Mathematics, University of Parma, Italy.
Possibly Not Closed Convex Polyhedra and the Parma Polyhedra Library.
R. Bagnara, E. Ricci, E. Zaffanella, P.M. Hill.
9th International Symposium on Static Analysis (SAS'02)
(Madrid, Spain, September 2002).
A New Encoding of Not Necessarily Closed Convex Polyhedra.
R. Bagnara, P.M. Hill, E. Zaffanella.
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.
Possibly Not Closed Convex Polyhedra
and the Parma Polyhedra Library.
R. Bagnara, E. Ricci, E. Zaffanella, P.M. Hill.
Technical Report.
Quaderno 286 (2002), Department of Mathematics, University of Parma, Italy.
Setsharing is redundant for pairsharing.
R. Bagnara, P.M. Hill, E. Zaffanella.
Theoretical Computer Science.
Soundness, Idempotence and Commutativity of SetSharing.
P.M. Hill, R. Bagnara, E. Zaffanella.
Theory and Practice of Logic Programming.
Decomposing NonRedundant Sharing by Complementation.
E. Zaffanella, P.M. Hill, R. 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.
P.M. Hill, E. Zaffanella, R. Bagnara.
Technical Report.
Quaderno 273 (2001), Department of Mathematics, University of Parma, Italy.
Boolean Functions for FiniteTree Dependencies.
R. Bagnara, E. Zaffanella, R. Gori, P.M. Hill.
8th International Conference on Logic for
Programming, Artificial Intelligence and Reasoning (LPAR'2001)
(Havana, Cuba, December 2001).
Correctness, Precision and Efficiency
in the Sharing Analysis of Real Logic Languages.
E. Zaffanella.
PhD thesis  School of Computing of
the University of Leeds, September 2001.
FiniteTree Analysis for Constraint LogicBased Languages.
R. Bagnara, R. Gori, P.M. Hill, E. Zaffanella.
8th International Symposium on Static Analysys (SAS'01),
(Paris, France, July 2001).
FiniteTree Analysis for Constraint LogicBased Languages.
R. Bagnara, R. Gori, P.M. Hill, E. Zaffanella.
Technical Report.
Quaderno 251 (2001), Department of Mathematics, University of Parma, Italy.
Boolean Functions for FiniteTree Dependencies.
R. Bagnara, E. Zaffanella, R. Gori, P.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.
R. Bagnara, P.M. Hill, E. Zaffanella.
7th International Conference on Logic for
Programming and Automated Reasoning (LPAR'2000)
(Reunion Island, France, November 2000).
Enhanced Sharing Analysis Techniques: A Comprehensive Evaluation.
R. Bagnara, E. Zaffanella, P.M. Hill.
2nd International ACM SIGPLAN Conference
on Principles and Practice of Declarative Programming (PPDP'00)
(Montreal, Canada, September 2000).
Efficient Structural Information Analysis for Real CLP Languages.
R. Bagnara, P.M. Hill, E. Zaffanella.
Technical Report.
Quaderno 229, Department of Mathematics, University of Parma, Italy.

[ToAppear]
~~~
[2020202x]
~~~
[20152019]
~~~
[20102014]
~~~
[20052009]
~~~
[20002004]
~~~
[19941999]

Published in 1999

Widening Sharing.
E. Zaffanella, R. Bagnara, P.M. Hill.
1st International Conference on Principles
and Practice of Declarative Programming (PPDP'99)
(Paris, France, September/October 1999).
Decomposing nonredundant sharing by complementation.
E. Zaffanella, P.M. Hill, R. Bagnara.
6th International Symposium on Static Analysis (SAS'99)
(Venice, Italy, September 1999).
Enhancing Sharing for precision.
R. Bagnara, E. Zaffanella, P.M. Hill.
APPIAGULPPRODE'99 Joint Conference on Declarative Programming
(L'Aquila, Italy, September 1999).
Widening Sharing.
E. Zaffanella, R. Bagnara, P.M. Hill.
APPIAGULPPRODE'99 Joint Conference on Declarative Programming
(L'Aquila, Italy, September 1999).

Published in 1998

The correctness of setsharing.
P.M. Hill, R. Bagnara, E. Zaffanella.
5th International Symposium on Static Analysis (SAS'98)
(Pisa, Italy, September 1998).
The correctness of setsharing.
P.M. Hill, R. Bagnara, E. Zaffanella.
1998 Joint Conference on Declarative Programming (APPIAGULPPRODE'98)
(A Coruña, Spain, July 1998).

Published in 1997

Abstracting Synchronization in Concurrent Constraint Programming.
E. Zaffanella, R. Giacobazzi, and Giorgio Levi.
The Journal of Functional and Logic Programming.
Setsharing is redundant for pairsharing.
R. Bagnara, P.M. Hill, E. Zaffanella.
4th International Symposium on Static Analysis (SAS'97)
(Paris, France, September 1997).
Sharing revisited.
R. Bagnara, P.M. Hill, E. Zaffanella.
1997 Joint Conference on Declarative Programming (APPIAGULPPRODE'97)
(Grado, Italy, June 1997).

Published in 1996

Modular Analysis of Suspension Free cc Programs.
E. Zaffanella.
1996 Joint Conference on Declarative Programming (APPIAGULPPRODE'96)
(DonostiaSan Sebastían, Spain, July 1996).
The ANDcompositionality of CLP computed answer constraints.
R. Bagnara, M. Comini, F. Scozzari, E. Zaffanella.
1996 Joint Conference on Declarative Programming (APPIAGULPPRODE'96)
(DonostiaSan Sebastían, Spain, July 1996).

Published in 1995

Domain Independent Ask Approximation in CCP.
E. Zaffanella.
1st International Conference on Principles
and Practice of Constraint Programming (CP'95)
(Cassis, France, September 1995).
Domain Independent Ask Approximation in CCP.
E. Zaffanella.
1995 Joint Conference on Declarative Programming (GULPPRODE'95)
(Marina di Vietri, Italy, September 1995).

Published in 1994

Abstracting Synchronization in Concurrent Constraint Programming.
E. Zaffanella, R. Giacobazzi, G. Levi.
6th International Symposium on Programming
Language Implementation and Logic Programming (PLILP'94)
(Madrid, Spain, September 1994).

[ToAppear]
~~~
[2020202x]
~~~
[20152019]
~~~
[20102014]
~~~
[20052009]
~~~
[20002004]
~~~
[19941999]

