Tools and libraries for static analysis and verification

Libraries

• Camllib: addition to OCaml standard libraries.
• Fixpoint: generic fixpoint engine in OCaml.
• APRON: numerical abstract domains library
• Bddapron: higher-level interface to (CUDD) BDDs, manipulaton of mixed Boolean/numerical formulas using BDDs, abstract domains combining BDDs and APRON domains.

Tools

• NBac: Numerical and Boolean Automaton Checker: a verification tool based on dynamic partitioning to verify safety properties of programs or systems. Connected to the LUSTRE synchronous language and Auto symbolic hybrid automata formalism.
• Interproc: an analyzer for an (academic) imperative language with recursion, that infers invariants about numerical variables.
• InterprocStack: an extension of Interproc, with both finite-type and numerical variables, and the choice between standard relational analysis, and an analysis using lattice automata [GJ07] for abstracting stacks.

Obsolete

• NewPolka: a library to handle convex polyhedra in any dimension, wiht a C and a OCaml interface. Now integrated in Apron.
• Formula: completely reorganized and renamed as Bdd/Bddapron.

Browsing subversion repository

You can browe directly the subversion repository. You can find more information about downloading from subversion repository.

Packages and distribution packages

The repository is organized as follows:

pkg/
pkg/camllib/
pkg/camllib/trunk/
pkg/camllib/branches/
pkg/camllib/branches/release-X.Y.Z
dist/
dist/interproc-dist/
dist/interproc-dist/trunk
dist/interproc-dist/branches/
...

The directory pkg contains the packages themselves, in isolation. Configuration is done using Makefile.config files (Makefile.config files belonging to different packages are compatible).

The directory dist contains distribution packages, that is, a main package together with the packages it requires to compile. Practically, these distribution packages are built from README and Makefile files, as well as external reference (in the sens of subversion) to packages themselves

Advice

If you have to compile from scratch a package like interproc that requires several libraries, the best is to check out interproc-dist which will in turn check out most needed libraries. Moreover, you'll have only one Makefile.config file to configure.

Otherwise, if you already have many required libraries installed, you may check out packages in isolation.

References

 [GJ07]

T. Le Gall and B. Jeannet. Lattice automata: a representation of languages over an infinite alphabet, and some applications to verification. In Static Analysis Symposium, SAS'07, volume 4634 of LNCS, August 2007.