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.