poster Home page

APRON numerical abstract domain library

About

The APRON library is dedicated to the static analysis of the numerical variables of a program by Abstract Interpretation. The aim of such an analysis is to infer invariants about these variables. like 1<=x+y<=z, which holds during any execution of the program. You may look at to the Interproc analyzer for an online demonstration of static analysis.

The APRON library is intended to be a common interface to various underlying libraries/abstract domains and to provide additional services that can be implemented independently from the underlying library/abstract domain, as shown by the poster on the right (presented at the SAS 2007 conference. You may also look at:

Currently, APRON provides a C interface and an OCaml interface. There also exists a C++ interface, which is more experimental.

The version 0.9.10 (10th septembre 2009) contains 3 libraries and 4 abstract domains:

It also provides an optional interface to the Parma Polyhedra Library, which adds

Demonstration

The online Interproc static analyzer illustrates the use of the APRON library in static analysis.

License

APRON is a free software under LGPL license, except the wrappers related to the PPL library, which follows the GPL license of the PPL library.

Documentation

Download

Requirements

Current version: 0.9.10

As the library may still contain subtle bugs, we strongly suggest to be up-to-date with the most recent version.

Older versions

References

 [JM09]
B. Jeannet and A. Miné. APRON: A library of numerical abstract domains for static analysis. In Computer Aided Verification, CAV'2009, volume 5643 of LNCS, pages 661-667, 2009.