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:

• the associated flyer;
• a 15 minutes presentation made at CAV 2009 conference in Grenoble [JM09];
• a detailed presentation by Antoine Miné.

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:

• The BOX intervals library
• The OCT octagon library
• The NEWPOLKA Convex Polyhedra and Linear Equalities library

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

• the Convex Polyhedra and Linear Congruences (grid) domains
• the reduced product of NewPolka convex polyhedra and PPL linear congruences

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

• Detailed presentation;
• On-line C interface and OCaml interface;
• C pdf or OCaml pdf;
• C example or OCaml example 1/OCaml example 2/OCaml example 3. For the ML examples, they are almost identical, but the ones with the higher numbers use higher-level functions to define affine expressions and constraints.

Download

Requirements

• An ANSI C compiler (only gcc with ansi option has been tested)
• The GMP library, version 4.2 or up, and the MPFR library, version 2.2 or up;
• Optionally, Parma Polyhedra Library, and GMP compiled with -enable-cxx configuration option)
• If you want the C++ interface (still experimental), GCC 4.1.2 or up
• If you want to use the OCaml interface, you need the OCaml system, version 3.09 or up, the CamlIDL 1.05 stub code generator for the OCaml interface, as well as GNU SED 4.1 or up, and GNU m4 (if you download from subversion repository). You also need MLGMPIDL, but it can be included if you opt for the "distribution" version of APRON (see below).

Current version: 0.9.10

• Tar-gzipped sources
• Tar-gzipped sources of both APRON and MLGMPIDL
• Changes
• You can also access to the (new) SUBVERSION REPOSITORY, by typing something like

  svn list scm.gforge.inria.fr/svnroot/apron.

  If you want to download to the last committed version:

  svn co scm.gforge.inria.fr/svnroot/apron/apron/trunk apron.

  If you want to access the distribution which references both APRON and MLGMPIDL (using subversion external links):

  svn co scm.gforge.inria.fr/svnroot/apron/apron-dist/trunk apron-dist.

  (the old repository http://svn.cri.ensmp.fr/svn/apron/ is obsolete)

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

Older versions

• 0.9.9 Tar-gzipped sources
• 0.9.8 Tar-gzipped sources
• 0.9.7 Tar-gzipped sources
• 0.9.6 Tar-gzipped sources
• 0.9.5 Tar-gzipped sources
• 0.9.4 Tar-gzipped sources
• 0.9.3 Tar-gzipped sources
• 0.9.2 Tar-gzipped sources
• 0.9.1 Tar-gzipped sources
• 0.9.0 Tar-gzipped sources

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.