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
• frontC
• 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.