This is Enea.

Home

Personal Info

Research

Papers

Teaching

About

DeliciousPPLite

[Page last updated on "novembre 22, 2020, 14:36:30".]

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.

Current version

  • 2020-11-24: PPLite 0.7 can be downloaded.
    New configuration option --enable-apron allows for compiling the wrapper for (the C language bindings of) the Apron interface. This version also adds a C++ polymorphic interface allowing to experiment with several variants of the domain of convex polyhedra: Poly, U_Poly, F_Poly, UF_Poly and their XXX_Stats versions, computing timing information for abstract operators.
  • Links to all versions released.

Support

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.

Main developers

  • Enea Zaffanella (supervisor)
  • Anna Becchi (former student)

Contributors and past members of development team

  • Gino Ceresini (former student)
  • Carlotta Colla (former student)
  • Maria Chiara Colla (former student)
  • Fabio Cristini (former student)
  • Eduard Ispas (former student)
  • Lorenzo Mora (student)
  • Riccardo Mori (student)
  • Sara Musiari (student)
  • Velia Pierdomenico (student)
  • Dana Greta Pop (student)
  • Luigi Zaccone (former student)

Papers and preprints

  1. A. Becchi and E. Zaffanella
    A Conversion Procedure for NNC Polyhedra
    CoRR, abs/1711.09593, November 2017
  2. A. Becchi and E. Zaffanella
    A Direct Encoding for NNC Polyhedra
    Proceedings of the 30th International Conference on Computer Aided Verification (CAV 2018) (Oxford, UK, July 2018)
  3. A. Becchi and E. Zaffanella
    An Efficient Abstract Domain for Not Necessarily Closed Polyhedra
    Static Analysis - 25th International Symposium (SAS 2018) (Freiburg, Germany, August 2018)
  4. A. Becchi and E. Zaffanella
    Revisiting Polyhedral Analysis for Hybrid Systems
    Static Analysis - 26th International Symposium (SAS 2019) (Porto, Portugal, October 2019)
  5. A. Becchi and E. Zaffanella
    PPLite: Zero-Overhead Encoding of NNC Polyhedra
    Information and Computation (2020).
  6. G. Frehse, A. Abate, D. Adzkiya, L. Bu, M. Giacobbe, M.S. Mufid, E. 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.
  7. 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
    ARCH-COMP19 Category Report: Hybrid Systems with Piecewise Constant Dynamics
    6th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH19) (Montreal, Canada, April 2019), EPiC Series in Computing.
  8. L. Bu, A. Abate, D. Adzkiya, M.S. Mufid, R. Ray, Y. Wu, E. Zaffanella
    ARCH-COMP20 Category Report: Hybrid Systems with Piecewise Constant Dynamics and Bounded Model Checking
    7th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH20) (Berlin, Germany, July 2020), EPiC Series in Computing.

Supervised theses (in Italian)

  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.
  2. Gino Ceresini
    Modernizzazione di codice C++: la libreria PPLite
    Undergraduate thesis, Department of Mathematical, Physical and Computer Sciences, University of Parma, Italy, December 2018.
  3. Carlotta Colla
    Un confronto tra implementazioni per insiemi di indici numerici
    Undergraduate thesis, Department of Mathematical, Physical and Computer Sciences, University of Parma, Italy, October 2020.
  4. Maria Chiara Colla
    Un'interfaccia a polimorfismo dinamico per la libreria PPLite
    Undergraduate thesis, Department of Mathematical, Physical and Computer Sciences, University of Parma, Italy, October 2020.
  5. Fabio Cristini
    Un confronto prestazionale tra librerie di calcolo numerico
    Undergraduate thesis, Department of Mathematical, Physical and Computer Sciences, University of Parma, Italy, September 2018.
  6. Eduard Ispas
    Implementazione del powerset dei poliedri convessi nella PPLite
    Undergraduate thesis, Department of Mathematical, Physical and Computer Sciences, University of Parma, Italy, September 2019.
  7. Lorenzo Mora
    Sviluppo software e debito tecnologico: un caso di studio
    Undergraduate thesis, Department of Mathematical, Physical and Computer Sciences, University of Parma, Italy, April 2020.
  8. Riccardo Mori
    Un'implementazione per l'inviluppo intero di poliedri razionali
    Undergraduate thesis, Department of Mathematical, Physical and Computer Sciences, University of Parma, Italy, September 2020.
  9. Sara Musiari
    Sull'applicabilità di tecniche di memoization alla libreria PPLite
    Undergraduate thesis, Department of Mathematical, Physical and Computer Sciences, University of Parma, Italy, September 2020.
  10. Dana Greta Pop
    Un caso di studio sull'integrazione di librerie per analisi statica: interfacciamento e debugging sistematico
    Undergraduate thesis, Department of Mathematical, Physical and Computer Sciences, University of Parma, Italy, April 2020.
  11. Luigi Zaccone
    La fattorizzazione cartesiana nella libreria PPLite
    Undergraduate thesis, Department of Mathematical, Physical and Computer Sciences, University of Parma, Italy, March 2019.

Available downloads

  • 2020-11-24: PPLite 0.7 can be downloaded.
    New configuration option --enable-apron allows for compiling the wrapper for (the C language bindings of) the Apron interface. This version also adds a C++ polymorphic interface allowing to experiment with several variants of the domain of convex polyhedra: Poly, U_Poly, F_Poly, UF_Poly and their XXX_Stats versions, computing timing information for abstract operators.
  • 2020-04-23: PPLite 0.6 can be downloaded. (No longer maintained: don't use it, switch to the most recent one).
    Added pplite::F_Poly, adding support for factored polyhedra (experimental feature, not optimized).
  • 2019-10-15: PPLite 0.5.1 can be downloaded. (No longer maintained: don't use it, switch to the most recent one).
    This version fixes a bug affecting Poly::parallel_affine_image() in version 0.5 (the bug was affecting computations of affine images when the denominators of the expressions where different from 1).
  • 2019-07-12: PPLite 0.5 can be downloaded (No longer maintained: don't use it, switch to the most recent one).
    Added helper class BBox to encode the (topologically closed, possibly infinite) bounding box of a polyhedron; this is used in new methods Poly::boxed_contains() and Poly::boxed_is_disjoint_from() so as to speed up computation (in particular, in client code computing over sets of polyhedra, as found in tools such as PHAVerLite).
  • 2019-03-08: PPLite 0.4.1 can be downloaded (No longer maintained: don't use it, switch to the most recent one).
    (Note: version 0.4.1 fixes a bug affecting Poly::hash() in version 0.4, which was released on 2019-03-03.) Added new method Poly::hash(), which can be used to quickly decide that two polyhedra are different. Added new method Poly::con_hull_assign(), computing the constraint hull of two polyhedra (note: the result depends on the specific constraint representation computed by the library). Improved the efficiency of the parallel affine image method. Corrected a few, corner case bugs (affected functionalities were: computation of the bhrz03 widening; the removal of space dimensions; the addition of generating lines).
  • 2018-10-09: PPLite 0.3 can be downloaded. (No longer maintained: don't use it, switch to the most recent one.)
    Added wrappers on the polyhedra domain: Poly_Stats collects time statistics on abstract operator calls; U_Poly improves the handling of unconstrained space dimensions. Corrected a few bugs: intersection of 0-dim polyhedra; printing of universe polyhedra; minimization of an affine function; a couple of other bugs in code used only in debugging mode.
  • 2018-07-10: PPLite 0.2 can be downloaded. (No longer maintained: don't use it, switch to the most recent one.)
    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.
  • 2018-05-08: PPLite 0.1 can be downloaded. (No longer maintained: don't use it, switch to the most recent one.)
    Initial release.
© Enea Zaffanella
enea.zaffanella@unipr.it

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