Little Roadmap of PPL Papers

The original research work that led to the creation of the Parma Polyhedra Library is described in several papers. These can be divided into two categories:

current references are those that we consider the best currently available sources for particular aspects of the library and of the theory upon which it is based;
historical references are those that have been superseded by more recent papers, but may still be interesting for reconstructing the history and evolution of ideas and techniques.

Current References

On the PPL in General

[BHZ08b]

R. Bagnara, P. M. Hill, and E. Zaffanella. 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):3-21, 2008.

This is the paper to read or cite if you are interested in or referring to the Parma Polyhedra Library in general: amongst other things, it explains the aim of the project and the main ideas behind it. You can use the following BibTeX entry:
@AT@Article{BagnaraHZ08SCP,
  Author = "R. Bagnara and P. M. Hill and E. Zaffanella",
  Title = "The {Parma Polyhedra Library}: Toward a Complete Set of Numerical
           Abstractions for the Analysis and Verification
           of Hardware and Software Systems",
  Journal = "Science of Computer Programming",
  Volume = 72,
  Number = "1--2",
  Pages = "3--21",
  Year = 2008,
}

On the Double Description Method

[BHZ05]

R. Bagnara, P. M. Hill, and E. Zaffanella. Not necessarily closed convex polyhedra and the double description method. Formal Aspects of Computing, 17(2):222-257, 2005.

This is the paper to read if you are interested in how we implement NNC polyhedra. It describes how the NNC polyhedra are embedded in a higher dimensional vector space so as to reuse the tools and techniques of the double description method. In particular, it defines a theoretically clean, high-level user interface and the specification of an efficient procedure for removing redundancies from the descriptions of NNC polyhedra.

On Widenings for Generic Convex Polyhedra

[BHRZ05]

R. Bagnara, P. M. Hill, E. Ricci, and E. Zaffanella. Precise widening operators for convex polyhedra. Science of Computer Programming, 58(1-2):28-56, 2005.

Read this paper if you are interested in widenings and extrapolations available in the PPL for the domain of convex polyhedra. After introducing the standard widening (methods in the library that are based on this have the prefix H79), it presents a framework for the systematic definition of new widening operators that are never less precise than a given widening. The framework is then instantiated on the domain of convex polyhedra so as to obtain a new improved widening operator (methods in the library that are based on this widening have the prefix BHRZ03). After presenting the well-known widening delay technique, the with tokens technique which is also supported by the PPL, is fully described.

On the Powerset Construction

[BHZ06b]

R. Bagnara, P. M. Hill, and E. Zaffanella. Widening operators for powerset domains. Software Tools for Technology Transfer, 8(4-5):449-466, 2006.

Read this paper if you are interested in using powersets to express disjunctive information. The paper describes the finite powerset construction which will upgrade any abstract domain to allow for the representation of finite disjunctions of its elements. The paper also defines some generic widening methodologies for this construction all of which upgrade a widening on the base-level domain. In particular, it describes the certificate-based widening method which is available as a templatic method in the PPL). Note that this is the first time that the problem of deriving non-trivial, provably correct widening operators in a domain refinement has been tackled successfully. The proposed techniques are illustrated by instantiating the widening methodologies on powersets of convex polyhedra, a domain for which no non-trivial widening operator was previously known (this instance is also fully supported by the PPL).

On Weakly Relational Domains

[BHZ09FMSD]

R. Bagnara, P. M. Hill, and E. Zaffanella. Weakly-Relational Shapes for Numeric Abstractions: Improved Algorithms and Proofs of Correctness. Formal Methods in System Design, 35(3):(279-323), 2009.

Read this paper if you are interested in using the weakly relational domains (the PPL supports the weakly relational domains of bounded difference shapes and octagonal shapes). These are domains for numerical abstractions that lie between (in terms of precision and efficiency) the domains of intervals and convex polyhedra. The variants provided by the PPL and described in this paper have several advantages, including algorithms of reduced complexity and provably correct widening operators.

On Applications of Polyhedral Computations

[BHZ09TCS]

R. Bagnara, P. M. Hill, and E. Zaffanella. Applications of Polyhedral Computations to the Analysis and Verification of Hardware and Software Systems. Theoretical Computer Science, 410(46):4672-4691, 2009.

Read this paper if you are interested in applications of polyhedral computations (such as the ones supported by the PPL) to the analysis and verification of hardware (yes, both of digital and analog devices) and software systems (including the analysis of imperative programs).

On Exact Join Detection

[BHZ10]

R. Bagnara, P. M. Hill, and E. Zaffanella. Exact join detection for convex polyhedra and other numerical abstractions. Computational Geometry: Theory and Applications, 43(5):453-473, 2010.

Read this paper if you are interested in the theory we developed for computing the exact join predicates provided by the PPL (exact join detection is the problem of deciding whether the least upper bound of two or more numerical abstractions is equal to their set-theoretic union).

On the Synthesis of Linear Ranking Functions

[BMPZ10]

R. Bagnara, F. Mesnard, A. Pescetti, and E. Zaffanella. 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/.

Read this paper if you are interested in synthesizing ranking functions for termination analysis. The two methods presented in this paper are fully implemented in the PPL and make it very easy to include termination-analysis capabilities in automatic program verifiers.

Historical References

On the PPL in General

[BRZH02a]

R. Bagnara, E. Ricci, E. Zaffanella, and P. M. Hill. Possibly not closed convex polyhedra and the Parma Polyhedra Library. In M. V. Hermenegildo and G. Puebla, editors, Static Analysis: Proceedings of the 9th International Symposium, volume 2477 of Lecture Notes in Computer Science, pages 213-229, Madrid, Spain, 2002. Springer-Verlag, Berlin.

This is the first published paper about the Parma Polyhedra Library in general.

[BRZH02b]

R. Bagnara, E. Ricci, E. Zaffanella, and P. M. Hill. Possibly not closed convex polyhedra and the Parma Polyhedra Library. Quaderno 286, Dipartimento di Matematica, Università di Parma, Italy, 2002. See also [BRZH02c]. Available at http://www.cs.unipr.it/Publications/.

This technical report is a preliminary version of the paper [BRZH02a].

On the Double Description Method

[BHZ03a]	R. Bagnara, P. M. Hill, and E. Zaffanella. A new encoding and implementation of not necessarily closed convex polyhedra. In M. Leuschel, S. Gruner, and S. Lo Presti, editors, Proceedings of the 3rd Workshop on Automated Verification of Critical Systems, pages 161-176, Southampton, UK, 2003. Published as TR Number DSSE-TR-2003-2, University of Southampton. This paper, which was presented at AVoCS 2003, is an earlier version of the paper [BHZ05].
[BHZ02b]	R. Bagnara, P. M. Hill, and E. Zaffanella. A new encoding of not necessarily closed convex polyhedra. In M. Carro, C. Vacheret, and K.-K. Lau, editors, Proceedings of the 1st CoLogNet Workshop on Component-based Software Development and Implementation Technology for Computational Logic Systems, pages 147-153, Madrid, Spain, 2002. Published as TR Number CLIP4/02.0, Universidad Politécnica de Madrid, Facultad de Informática. This workshop paper is a preliminary version of the paper [BHZ03a].
[BHZ02TR]	R. Bagnara, P. M. Hill, and E. Zaffanella. 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/. This technical report is a preliminary version of the paper [BHZ03a].