Fluctuat is an abstract-interpretation based static analyzer of numerical programs (C or Ada) developed since 2001. Given sets of inputs and parameters, possibly entached by uncertainties, it considers all possible behaviours of a numerical program both in real and in finite precision, and characterizes the differences.


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.