POPACheck
A model checker for probabilistic pushdown automata. Designed for formal verification of systems with recursive probabilistic behavior.
CPSDebug
A tool for explaining failures in cyber-physical systems by combining testing, specification mining, and failure analysis.
POLAR
An algebraic analyzer for (probabilistic) loops using recurrence solving and invariant inference.
Amber
A probabilistic termination tool combining martingale theory with asymptotic bounding techniques to analyze while-programs.
MoonLight
A lightweight tool for monitoring spatio-temporal properties of mobile and distributed systems using STREL logic.
FIM
fault injection and mutation for Simulink.
HyperProb
A Model Checker for Probabilistic Hyperproperties.
ShapeIt
A tool for Mining Shape Expressions