PV3 STLmcchecks whether STL properties hold for a given hybrid system

Application domain/field

Type of tool

Model checker

Expected input


Expected output

Whether the properties hold or not. If not, a counterexample can be shown.


The tool can be used to verify that, up to given bounds, the robustness degree of an STL formula φ is greater than a robustness threshold ϵ>0 for all possible behaviors of the ysstem. This is done by reducing the STL model checking problem to Boolean STL model checking using ϵ-strengthening. It uses SMT solvers such as Z3, Yices2 and dReal.
Model checking STL


Related papers

STLmc: Robust Model Checking of Hybrid Systems Using SMT (CAV 2022)

Last publication date

7 August 2022

ProVerB specific

Markdown description: view/edit

ProVerB is a part of SLEBoK. Last updated: February 2023.