Tools

Fluctuat

Fluctuat is a static analyzer of numerical programs (C or Ada) developed since 2001 at CEA LIST, and then at École Polytechnique in collaboration with CEA LIST. Given sets of inputs and parameters, possibly with by uncertainties, it considers all possible behaviors of a numerical program both in real and in finite precision, and characterizes the differences. It is based on abstract interpretation, mainly using the abstract domain of zonotopes. It has been used in various industrial test-cases, and is currently being extended in order to handle inner approximations and non-deterministic/probabilistic information.

Alcool

Alcool is a static analyzer of concurrent programs based on directed geometric models. It mainly focuses on issues related to the presence of concurrency such as the detection of deadlocks or unreachable code. It is based on the construction of the so-called “geometric model” for programs, as well as associated computations (the category of components, etc.). It is currently being redeveloped from scratch, both in order to improve its architecture and to have a version which can be distributed under an open-source license.

CaTT

CaTT is a proof assistant for weak higher categories, in the globular variant of the definition. It is based on a type theory which allows to check that a morphism is well-defined by type inference.

IbexCont

IbexCont is plugin for Ibex implementing a rigorous continuation of one dimensional manifolds implicitly defined by a system of equations with n variables and n-1 equations.

RHINO

RHINO is a library to compute guaranteed inner and outer approximations of reachable sets for uncertain continous-time dynamical systems, with (possibly time-varying) perturbations and control inputs.

and more…

Other developments of the team can be found on our GitHub page.