An SMT-based bounded model checker for signal temporal logic

Navigation

Verified details

These details have been verified by PyPI
Project links
GitHub Statistics
Maintainers
Avatar for rgyenr2 from gravatar.com rgyenr2

Unverified details

These details have not been verified by PyPI
Project links
Meta
  • License: GPLv3
  • Author: Geunyeol Yu
  • Tags stlmc, model checker, STL, signal temporal logic, bounded model checker
  • Requires: Python >=3.8
Classifiers

Project description

STLmc

STLmc is an SMT-based bounded model checker for signal temporal logic (STL) of hybrid systems. The algorithm of the tool is refutationally complete for STL properties of bounded signals.

For more information about STLmc, please visit our website

Features

  • Bounded model checking
  • Generating trajectories that falsify the given STL properties if any exists
  • Supporting various SMT solvers (e.g., Z3, Yices2, dReal3)

Project details

Verified details

These details have been verified by PyPI
Project links
GitHub Statistics
Maintainers
Avatar for rgyenr2 from gravatar.com rgyenr2

Unverified details

These details have not been verified by PyPI
Project links
Meta
  • License: GPLv3
  • Author: Geunyeol Yu
  • Tags stlmc, model checker, STL, signal temporal logic, bounded model checker
  • Requires: Python >=3.8
Classifiers

Release history Release notifications | RSS feed

This version

1.0.0.dev2 pre-release

1.0.0.dev1 pre-release

Download files

Download the file for your platform. If you're not sure which to choose, learn more about installing packages.

Source Distribution

stlmc-1.0.0.dev2.tar.gz (5.1 MB view hashes)

Uploaded Source

Built Distributions

stlmc-1.0.0.dev2-cp312-cp312-manylinux_2_5_x86_64.manylinux1_x86_64.whl (4.1 MB view hashes)

Uploaded CPython 3.12 manylinux: glibc 2.5+ x86-64

stlmc-1.0.0.dev2-cp312-cp312-macosx_14_0_arm64.whl (3.2 MB view hashes)

Uploaded CPython 3.12 macOS 14.0+ ARM64

stlmc-1.0.0.dev2-cp311-cp311-manylinux_2_5_x86_64.manylinux1_x86_64.whl (4.1 MB view hashes)

Uploaded CPython 3.11 manylinux: glibc 2.5+ x86-64

stlmc-1.0.0.dev2-cp311-cp311-macosx_14_0_arm64.whl (3.2 MB view hashes)

Uploaded CPython 3.11 macOS 14.0+ ARM64

stlmc-1.0.0.dev2-cp310-cp310-manylinux_2_5_x86_64.manylinux1_x86_64.whl (4.1 MB view hashes)

Uploaded CPython 3.10 manylinux: glibc 2.5+ x86-64

stlmc-1.0.0.dev2-cp310-cp310-macosx_14_0_arm64.whl (3.2 MB view hashes)

Uploaded CPython 3.10 macOS 14.0+ ARM64

stlmc-1.0.0.dev2-cp39-cp39-manylinux_2_5_x86_64.manylinux1_x86_64.whl (4.1 MB view hashes)

Uploaded CPython 3.9 manylinux: glibc 2.5+ x86-64

stlmc-1.0.0.dev2-cp39-cp39-macosx_14_0_arm64.whl (3.2 MB view hashes)

Uploaded CPython 3.9 macOS 14.0+ ARM64

stlmc-1.0.0.dev2-cp38-cp38-manylinux_2_5_x86_64.manylinux1_x86_64.whl (4.1 MB view hashes)

Uploaded CPython 3.8 manylinux: glibc 2.5+ x86-64

stlmc-1.0.0.dev2-cp38-cp38-macosx_14_0_arm64.whl (3.2 MB view hashes)

Uploaded CPython 3.8 macOS 14.0+ ARM64

Supported by

AWS AWS Cloud computing and Security Sponsor Datadog Datadog Monitoring Fastly Fastly CDN Google Google Download Analytics Microsoft Microsoft PSF Sponsor Pingdom Pingdom Monitoring Sentry Sentry Error logging StatusPage StatusPage Status page