This is Enea.


Personal Info






[Page last updated on "settembre 04, 2018, 11:42:46".]

Welcome to the PPLite home page.

PPLite is an open-source C++ library implementing the abstract domain of convex polyhedra, to be used in tools for static analysis and verification.


  • PPLite 0.2 can be downloaded.
    Added support for (conditional) thread safety: it is now possible to develop multithreaded applications using PPLite. Implemented a few other operators on the polyhedra domain, including the more precise bhrz03 widening.
  • PPLite 0.1 can be downloaded.
    Initial release, no longer maintained. Don't use it, switch to the most recent one.


If you need help for using PPLite or have some feature requests, ask me.

Goals (and non-goals)

While being derived from the PPL (Parma Polyhedra Library), PPLite has a very different goal: to provide researchers and students with a lightweight framework for experimenting with new ideas and algorithms in the context of polyhedral computations. In particular, PPLite is not aimed at implementing the full range of abstract domains and operators made available by the PPL. The main characteristics of PPLite are the following.
  • Both closed and NNC rational convex polyhedra are supported.
  • Exact computations are based on FLINT.
  • Performance is important, but not the main concern (ease of implementation and readability are given priority).
  • Portability is important, but not the main concern (ease of implementation and readability are given priority).
  • The library is written in modern C++. The developers should feel free to use language features made available by the recent standards, provided these lead to a simpler implementation or improve on code readability.
  • The library is meant to be lightweight from the point of view of the developers: the goal is to reduce maintenance costs. This implies, among other things:
    • backward compatibility is a non-goal;
    • documentation is kept minimal (if not omitted altogether);
    • there is no plan to provide foreign language interfaces;
    • the library typically provides narrow contracts: preconditions on operators are not checked at runtime, so that user errors will lead to undefined behavior (rather than exceptions);
    • encapsulation is not fully enforced: a knowledgeable user can directly change the contents of inner data structures, e.g., to experiment with alternative implementations of domain operators.

Development team

  • Enea Zaffanella (main developer, supervisor)
  • Anna Becchi (main developer, former student)
  • Gino Ceresini (contributor, current student)
  • Fabio Cristini (contributor, current student)

Papers, theses, etc.

  1. Anna Becchi
    Poliedri NNC: una nuova rappresentazione e algoritmo di conversione
    Undergraduate thesis, Department of Mathematical, Physical and Computer Sciences, University of Parma, Italy, September 2017. In Italian.
  2. Anna Becchi and Enea Zaffanella
    A Conversion Procedure for NNC Polyhedra
    CoRR, abs/1711.09593, November 2017
  3. Anna Becchi and Enea Zaffanella
    A Direct Encoding for NNC Polyhedra
    Proceedings of the 30th International Conference on Computer Aided Verification (CAV 2018) (Oxford, UK, July 2018)
  4. Goran Frehse, Alessandro Abate, Dieky Adzkiya, Lei Bu, Mirco Giacobbe, Muhammad Syifa'ul Mufid, Enea Zaffanella
    ARCH-COMP18 Category Report: Hybrid Systems with Piecewise Constant Dynamics
    5th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH18) (Oxford, UK, July 2018), EPiC Series in Computing.
  5. Anna Becchi and Enea Zaffanella
    An Efficient Abstract Domain for Not Necessarily Closed Polyhedra
    Static Analysis - 25th International Symposium (SAS 2018) (Freiburg, Germany, August 2018)
© Enea Zaffanella

| Home | Personal Info | Research | Papers | Teaching | About