| Tool | Features |
|---|---|
| APRON | Numerical abstract domain library |
| HyMITATOR | Extension of IMITATOR to hybrid systems |
| HyTech | Reachability analysis for hybrid 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 |
| Uppaal | Modeling, validation and verification of real-time systems modeled as timed automata |