| Tool | Features |
|---|---|
| APRON | Numerical abstract domain library |
| HyMITATOR | Extension of IMITATOR to hybrid systems |
| HyTech | Reachability analysis for hybrid automata |
| JANI | The JANI Specification for networks of various kinds of quantitative automata |
| MAP | A tool for transformation of logic programs using the unfold/fold methodology |
| PAT | Specification, simulation and model checker for multiple formalisms |
| PHAVer | Polyhedral Hybrid Automaton Verifyer |
| PPL | The Parma Polyhedra Library, used by IMITATOR |
| Prism | Probabilistic symbolic model checker |
| PSyHCoS | Parameter Synthesis for Hierarchical Concurrent Systems |
| RED library | Extending BDD technology to dense-time spaces |
| Roméo | A tool for (parametric) Time Petri Nets analysis |
| ShrinkTech | A tool evaluating the robustness (wrt shrinking) in timed automat |
| SpaceEx | State Space Explorer for Hybrid Systems |
| Uppaal | Modeling, validation and verification of real-time systems modeled as timed automata |
| WSN-PN | Modeling, validation and verification of Petri nets models |