This is Enea.

Home

Personal Info

Research

Papers

Teaching

About

DeliciousPPLite

[Page last updated on "giugno 08, 2018, 12:00:42".]

Welcome to the PPLite home page.

News: PPLite 0.1 can be downloaded.

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

While being derived from the PPL (Parma Polyhedra Library), it 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. Some of its main characteristics 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
    To appear in Proceedings of the 30th International Conference on Computer Aided Verification (CAV 2018) (Oxford, UK, July 2018)
  4. Anna Becchi and Enea Zaffanella
    An Efficient Abstract Domain for Not Necessarily Closed Polyhedra
    To appear in Static Analysis - 25th International Symposium (SAS 2018) (Freiburg, Germany, August 2018)
© Enea Zaffanella
enea.zaffanella@unipr.it

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