Fixpoint

About

Fixpoint is an OCaml library implementing a generic fixpoint engine. The interface is parameterized by the abstract domain on which fixpoint computations are performed.

A short presentation in french

The fixpoint solver library is composed of several modules.

• Fixpoint: this is the only module to look at for a normal user.
• example.ml: example of use of the library;
• FixpointType: defines the various types and associated printing functions (including for the DOT output);
• FixpointStd: implements the Kleene-Bourdoncle iteration technique [Bou93] (combined with working-set algorithm) for solving equations described explicitly by an hypergraph, and offers base functions for the more sophisticated techniques;
• FixpointGuided: implements the Gopan-Reps guided iteration technique [GR07] for equations described explicitly by an hypergraph;
• FixpointDyn: exploits an implicit description (under the form if a successor function) of the equation graph, which is then explored dynamically by alternating propagation phase (to detect newly non-empty variables) and upto-convergence-iteration phase.
• FixpointThreshold: implements the threshold inference algorithm of [LCJG11].

License

LGPL license (GNU Library General Public License).

Download

Current version: 2.3.2

• Subversion repository: Fixpoint alone (see Up for the organisation of the repository)
• Subversion repository: Fixpoint together with dependency camllib (see Up for the organisation of the repository)

Documentation

• PDF with a small introduction
• On-line
• Example file

References

 [Bou93]

F. Bourdoncle. Efficient chaotic iteration strategies with widenings. In International Conference on Formal Methods in Programming and their Applications, volume 735 of LNCS, 1993.

 [GR07]

Denis Gopan and Thomas W. Reps. Guided static analysis. In Static Analysis Symposium, SAS'07, volume 4634 of LNCS, August 2007.

 [LCJG11]

Lies Lakhdar-Chaouch, Bertrand Jeannet, and Alain Girault. Widening with thresholds for programs with complex control graphs. In Automated Technology for Verification and Analysis, ATVA'11, volume 6996 of LNCS, pages 492-502, 2011.