Lustre V6 is the last version of the academic Lustre compiler, featuring an ada-like package mechanism, structured data-types (enums, structures), array iterators, and static recursion.
A timing analysis tool for multi-core: From a description of data-flow application and initial schedule and mapping, it produces an updated schedule (release dates) that takes into account the inter-task interference. The focus is on the interference due to shared bus.
PADEC is a framework to build certified proofs of self-stabilizing algorithms using the Coq proof assistant. The framework includes the definition of the computational model, lemmas for common proof patterns and case studies. A constant purpose was to convince the designers that what we formally prove using PADEC is what they expect by using definitions that are (syntactically) as close as possible to their usual definitions.
rdbg is now part of the Lustre V6 toolbox (lus2lic, lurette, rdbg)
SASA is a Self-stabilizing Algorithms SimulAtor, based on the so-called Atomic State model (ASM) introduced by Dijkstra in its seminal article on Self-stabilizing distributed algorithms.
A version of the CompCert certified compiler with added optimizations and a backend for the Kalray KVX processor.