Forge
APR Software
OMicroB : OCaml on Microcontroller Boards
OMicroB is a specialized implementation of the OCaml virtual machine designed to run on resource-constrained microcontrollers. This implementation can indeed run non-trivial OCaml programs on small microcontrollers, and provides the embedded software developer with all the high-level programming paradigms of the OCaml language (functional, imperative, modular, object-oriented) as well as increased security through static typing and automatic memory management. The OMicroB compilation chain takes a byte-code executable directly produced by the OCaml compiler and after several analysis passes (dead code detection, partial evaluation, ...) produces a C code embedding the VM, its execution library and the transformed byte-code. This produced C code, highly portable, targets different microcontroller architectures and can be compiled and executed on a standard PC for simulation and debugging purposes.
Project Leader : Emmanuel CHAILLOUX
04/2023
MOPSA analyzer : MOPSA Static Analyzer
MOPSA is a multi-language program verification software based on sound static analysis by abstract interpretation. It automatically infers invariants and detects, at compile time, the possible run-time errors. The analysis computes an interpretation of programs in a collection of reusable abstractions programmed in OCaml. Thanks to its modular conception, MOPSA can be easily extended in the set of properties and the set of analyzed languages. MOPSA currently supports significant subsets of the C and Python 3 languages. In C, MOPSA detects undefined behaviors as well invalid calls to the standard C library (specified in a dedicated modelization language). In Python, MOPSA, performs a type, value, and exception analysis.
Project Leader : Antoine Miné
03/2018
TTK : Topology ToolKit
The Topology ToolKit (TTK) is an open-source library and software collection for topological data analysis and visualization. TTK can handle scalar data defined either on regular grids or triangulations, in 2D, 3D, or more. It provides a substantial collection of generic, efficient and robust implementations of key algorithms in topological data analysis.
Project Leader : Julien Tierny
04/2017
piexplorer : an explicit state-space generation tool and a model-checker for the Pi-calculus
The problem of generating an explicit state-space for the pi-calculus is a complex problem. As of today, there exists only two tools with this functionality : the HAL laboratory and pi-explorer. The latter is based on a symbolic semantics that is much more economical than the early semantics as implemented by HAL. A model checker is also associated to the tool, but it is possible to use external tools based on the state graphs generated by the pi-explorer. These tools are based on recent works of the APR team (the pi-graphs), in a collaboration with university of Evry and université libre de Bruxelles.
Project Leader : Frédéric PESCHANSKI
09/2015
LaTTe : a laboratory of type theory experiments
LaTTe is a proof assistant library based on type theory. The specific feature of LaTTe is its design as a library (unlike most proof assistant, generally designed as standalone tools) tightly integrated with the Clojure language and ecosystem. This enables "proving in the large": sharing mathematical contents across the internet in a collaborative way. It also provides a domain specific language for declarative proofs, based on "fitch-style" proofs for natural deduction. The tool is developed by members of the APR team in a collaboration with the Whisper team (Pierre-Evariste Dagand).
Project Leader : Frédéric PESCHANSKI
03/2015
PENDULUM : OCaml syntax extension dedicated to the programming of reactive systems on the Web
Pendulum is a language dedicated to the programming of reactive systems on the Web. It has a powerful expressivity to describe synchronous concurrent systems communicating with broadcast signals. Its constructions and implementation are mostly based on Esterel. The language is embedded in OCaml as a syntax extension. It allows the programmer to describe reactive machines as OCaml values, and run them on signal arguments. The execution of concurrency in pendulum is completely sequential and the scheduling is static. (similar work and inspiration)
Project Leader : Rémy EL SIBAE
11/2014
AbSolute : AbSolute
AbSolute is a constraint solver based on abstract domains.
It implements the resolution method presented in the article: (VMCAI), Rome, Italy, 2013 [Article] [Article in French] Antoine Miné, Charlotte Truchet, Frédéric Benhamou, Constraint Solver based on Abstract Domains, 14th International Conference on Verification,
This solver can solve continuous, discrete and mixed problems (containing both integer and real variables) and proposes techniques for processing both linear and non-linear constraints. Rounding errors are taken into account during the resolution. The solver calculates sound float approximations of the real solutions of a problem. AbSolute uses Apron, an Ocaml library of abstract domains, which solves problems using other abstract domains than intervals.
Project Leader : Marie PELLEAU
11/2011
Arbogen : a fast uniform random tree generator
Arbogen is a fast uniform random generator of tree structures. The tool reads a grammar file describing a tree structure (e.g. binary trees, 2-3-4 trees, etc.) and a size interval (eg. trees of size 1000+-100). From the grammar one or many trees satisfying the structure and the size interval are produced. The generated tree are generated with a guarantee of uniformity, which means that it is the "average" tree for the given size. The tool relies on advanced algorithms based on Boltzman sampling, based on recent APR research works (in the realm of ANR Magnum 2010-2014).
Project Leader : Frédéric PESCHANSKI
10/2011
SPOC : Strem Processing with OCaml
SPOC is a set of tools for GPGPU programming with OCaml.
The SPOC library enables the detection and use of GPGPU devices with OCaml using Cuda and OpenCL. There is also a camlp4 syntax extension to handle external Cuda or OpenCL kernels, as well as a DSL (called Sarek) to express GPGPU kernels from the OCaml code.
Project Leader : Mathias BOURGOIN
09/2010