- Prelude is a synchronous data-flow language with real-time constraints. Prelude programs are compiled into multi-thread C code. The language and its compiler are developed in collaboration with ONERA Toulouse.
- PTASK is a library for programming real-time systems in Linux. It serves as the target RTOS API in the SYCOMORES project. The PTASK library is authored by Giuseppe Lipari. It has been initially developed to support teaching real-time systems at the Scuola Sant’Anna. It has later been extended with additional capabilities and it is being used as target for design tools such as CPAL19 from RTaW20 and by other companies.
- Catala is a domain-specific programming language designed for deriving correct-by-construction implementations from legislative texts. Its specificity is that it allows direct translation from the text of the law using a literate programming style, that aims to foster interdisciplinary dialogue between lawyers and software developers. By enjoying a formal specification and a proof-oriented design, Catala also opens the way for formal verification of programs implementing legislative specifications.
- Mopsa is an open-source static analysis platform relying on abstract interpretation. It provides a novel way to combine abstract domains, in order to offer extensibility and cooperation between them, which is especially beneficial when relational numerical domains are used. It is able to analyze C, Python, and programs mixing these two languages. Mopsa was originally developed at LIP6, Sorbonne Université following an ERC Consolidator Grant award to Antoine Miné. It is now partially developed at Inria.
- A date calculation library with a well-defined semantics
- WSymb is a WCET analysis tool. Its main specificity is that, instead of a constant WCET, it computes a *WCET formula*, where symbols (or parameters) can correspond to various values unkown at analysis time. The formula can later be instanciated, when parameter values are known.
- Polymalys is a tool for static analysis of binary code. It discovers linear relations between data locations (i.e. memory locations as well as registers) of the code. The analysis relies on abstract interpretation using a polyhedra-based abstract domain. The current main application is Worst-Case Execution Time analysis in combination with the WSymb tool.
- A Coq library for defining and reasoning about partial (co)recursive functions.