Introduction to APRON

The APRON library provides a common interface for abstract domains of invariants for numerical variables, in the sense of the Abstract Interpretation theory. It includes a few domains, and provides interfaces to libraries implemented by other teams.

Several libraries already exists, wich implement various abstract domains of invariants. One can cite intervals, linear equalities, octagons, octahedra, convex polyhedra, polynomial equalities, polynomial inequalities. Although they offer a kernel of common functionalities, their API may differ greatly, and some functionalities may lack in some libraries. The aim of the APRON library is to offer a common interface to these libraries. Such a standardized interface offers several advantages: it allows

• to easily substitute a library/abstract domain by another in the same analysis tool; this is useful to compare the efficiency of 2 implementations of the same abstract domain, or the precision of 2 different abstract domains.
• to factorize services which are mostly independant of the abstract domain (variables management, linearization of non-linear expressions, etc...);
• to make easier the combination of abstract domains: the abstract domains to be combined are used through the same interface, as the resulting combination;

As a user, why should I use APRON ?

1. it makes very easy to switch the abstract domain (for numerical variables) in use in an analyzer;
2. it already offers the most used abstract domains, ranging from intervals, octagons, convex polyhedra to linear congruences;
3. its interface should satisfy most needs, as it already satisfies the members of the APRON project working in different contexts (verification of high-level specifications/programs with exact arithmetics for INRIA \& Verimag, static analysis of runtime errors with floating-point arithmetics for ENS Paris, automatic parallelization of programs for ENSMP).
4. the interface, at the level 1, already provides slightly higher-level functionalities than most existing and publicy available abstract domains libraries (with the manipulation of environments); this statement should be reinforced in the near future with the planned addition of a generic non-linear expressions layer and a floating-point arithmetic layer.

As a domain implementor, why should I interface my abstract domain/library to APRON ?

1. to incite existing users of the APRON interface to try your library;
2. to make your users, including yourself, benefit from previous points 1 and 4;
3. to not waste your time implementing environments, variables renaming, OCaml interfaces, and so on; the effort to connect your library to the interface should at minimum be counterbalanced by such gains;