We are developing (or have developed) several tools, most of them available as open-source software:
- OTAWA: a toolset dedicated to Worst-Case Execution Time analysis
- oRange: a tool that determines loop bounds in C programs
- Choregies: demonstrator for a high-precision symbolic loop bound analyzer
- pathFinder: a tool to detect infeasible paths. It produces an .ffx (format defined by TRACES for annotations) file of constraints that can by used by OTAWA.