STLMC

 _____  _____  _
/  ___||_   _|| |
\ `--.   | |  | |     _ __ ___    ___
 `--. \  | |  | |    | '_ ` _ \  / __|
/\__/ /  | |  | |____| | | | | || (__
\____/   \_/  \_____/|_| |_| |_| \___|

STLmc is an SMT-based bounded model checker for signal temporal logic (STL) properties of hybrid systems. It supports linear, polynomial, and ODE dynamics through Z3, Yices2, and dReal3. STLmc provides robust STL model checking and bounded reachability checking, with one-step or two-step solving and symbolic or explicit transition-path exploration. It can generate counterexamples for violated STL properties and witnesses for reachable targets, which can be inspected as interactive graphs or human-readable text reports.

Bug report

If you encounter any issues while using STLmc, please submit a bug report through GitHub Issues https://github.com/stlmc/stlmc/issues. Please include enough information in your bug report to enable us to reproduce and fix the problem.