APRON

Numerical Abstract Domain Library

  Introduction | Contents | Code 🔗 | API Documentation | Resources 

Introduction

Apron is a library to represent properties of numeric variables, such as variable bounds or linear relations between variables, and to manipulate these properties through semantic operations, such as variable assignments, tests, conjunctions, entailment.

Apron is intended to be used in static program analyzers, in order to infer invariants of numeric variables, i.e., properties that hold for all executions of a program. It is based on the theory of Abstract Interpretation.

The library is open-source, and hosted on GitHub.

Library Contents

The Apron library includes several numeric abstract domains, corresponding to different classes of numeric properties with their own internal representation and algorithms, achieving various trade-offs between precision, expressiveness, and efficiency.

Apron includes the following numeric domains: intervals (boxes), polyhedra (newpolka), octagons, zonotopes (taylor1plus). Additional domains are made available through the optional PPL third-party library: alternate polyhedra implementation, grids, reduced products of polyhedra and grids.

The domains are made available under a common interface, so that changing the abstract domain of interpretation in a static analysis should only take a one-line change.

The core API is in C, but optional API wrappers for additional languages are provided: OCaml, Java, C++.

API Documentation

Some documentations are not up-to-date. However, the API is pretty stable.

• C API, also in PDF form (main API)
• OCaml API
• Java API
• C++ API (not much used)

Additional Resources

Presentations and articles about Apron:

• Apron flyer
• Apron poster
• slides from a detailed presentation
• reference article (at CAV 2009)

Some projects that use Apron:

• the Interproc analyzer