AMT 2.0 is a tool for offline monitoring and measuring temporal specifications over discrete and continuous behaviors.
Kronos is a tool for model-checking of timed automata against specifications expressed using the real-time temporal logic TCTL.
This library provides an algorithmic infrastructure for reachability computation of non-linear dynamical systems.
PHAVer is a tool for reachability analysis of continuous and hybrid systems based on Linear Hybrid Automata.
The SpaceEx platform, a tool designed to facilitate the implementation of algorithms related to reachability and safety verification of continuous and hybrid systems.
d/dt is a prototype tool for reachability analysis of continuous and hybrid systems
Montre is a monitoring tool to search patterns specified by timed regular expressions over real-time behaviors. It uses timed regular expressions as a compact, natural, and highly-expressive pattern specification language for monitoring applications involving quantitative timing constraints. The tool essentially incorporates online and offline timed pattern matching algorithms so it is capable of finding all occurrences of a given pattern over both logged and streaming behaviors. (...)
This library implements an algorithm for learning the boundary between an upward-closed set X1 and its downward-closed component X2 (i.e., X=X1+X2). Generally, the library supports spaces X of dimension N. The algorithm selects sampling points x=(x1,x2,...,xN) for which it submits membership queries ’is x in X1 ?’ to an external Oracle. Based on the Oracle answers and relying on monotonicity, the algorithm constructs an approximation of the boundary, called the Pareto front. The algorithm (...)
Dataflow multi-core scheduling using SMT solvers.
OpenKronos : is an on-the-fly verification tool for timed automata based on an integration of the DBM library of Kronos into CADP.