Skip to main content

An SMT-based bounded model checker for signal temporal logic

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


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.dev3.tar.gz (5.1 MB view details)

Uploaded Source

Built Distributions

If you're not sure about the file name format, learn more about wheel file names.

stlmc-1.0.0.dev3-cp312-cp312-manylinux_2_5_x86_64.manylinux1_x86_64.whl (4.1 MB view details)

Uploaded CPython 3.12manylinux: glibc 2.5+ x86-64

stlmc-1.0.0.dev3-cp312-cp312-macosx_14_0_arm64.whl (3.2 MB view details)

Uploaded CPython 3.12macOS 14.0+ ARM64

stlmc-1.0.0.dev3-cp311-cp311-manylinux_2_5_x86_64.manylinux1_x86_64.whl (4.1 MB view details)

Uploaded CPython 3.11manylinux: glibc 2.5+ x86-64

stlmc-1.0.0.dev3-cp311-cp311-macosx_14_0_arm64.whl (3.2 MB view details)

Uploaded CPython 3.11macOS 14.0+ ARM64

stlmc-1.0.0.dev3-cp310-cp310-manylinux_2_5_x86_64.manylinux1_x86_64.whl (4.1 MB view details)

Uploaded CPython 3.10manylinux: glibc 2.5+ x86-64

stlmc-1.0.0.dev3-cp310-cp310-macosx_14_0_arm64.whl (3.2 MB view details)

Uploaded CPython 3.10macOS 14.0+ ARM64

stlmc-1.0.0.dev3-cp39-cp39-manylinux_2_5_x86_64.manylinux1_x86_64.whl (4.1 MB view details)

Uploaded CPython 3.9manylinux: glibc 2.5+ x86-64

stlmc-1.0.0.dev3-cp39-cp39-macosx_14_0_arm64.whl (3.2 MB view details)

Uploaded CPython 3.9macOS 14.0+ ARM64

stlmc-1.0.0.dev3-cp38-cp38-manylinux_2_5_x86_64.manylinux1_x86_64.whl (4.1 MB view details)

Uploaded CPython 3.8manylinux: glibc 2.5+ x86-64

stlmc-1.0.0.dev3-cp38-cp38-macosx_14_0_arm64.whl (3.2 MB view details)

Uploaded CPython 3.8macOS 14.0+ ARM64

File details

Details for the file stlmc-1.0.0.dev3.tar.gz.

File metadata

  • Download URL: stlmc-1.0.0.dev3.tar.gz
  • Upload date:
  • Size: 5.1 MB
  • Tags: Source
  • Uploaded using Trusted Publishing? Yes
  • Uploaded via: twine/6.0.1 CPython/3.12.8

File hashes

Hashes for stlmc-1.0.0.dev3.tar.gz
Algorithm Hash digest
SHA256 456abb4650b2845ff58cb30dd9db9cfbd2310423a9331a07127a8a4e45584f01
MD5 f5bd7877d6b2864e8e5139a44b908472
BLAKE2b-256 2f1075bcd94774d67c3415f7eeb2b15541afd6449f46fe453ab7da64ac25acc6

See more details on using hashes here.

Provenance

The following attestation bundles were made for stlmc-1.0.0.dev3.tar.gz:

Publisher: release.yml on stlmc/stlmc

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

File details

Details for the file stlmc-1.0.0.dev3-cp312-cp312-manylinux_2_5_x86_64.manylinux1_x86_64.whl.

File metadata

File hashes

Hashes for stlmc-1.0.0.dev3-cp312-cp312-manylinux_2_5_x86_64.manylinux1_x86_64.whl
Algorithm Hash digest
SHA256 4f4707c868190257807735a39ad2bf07e202197514d332fa36fb134eff81353f
MD5 1257dab0ba03b130542e1031e98a5744
BLAKE2b-256 8a0413de58229e4567ea0edee228222c090dd5aa648e36349f9de49ed1fc0cbf

See more details on using hashes here.

Provenance

The following attestation bundles were made for stlmc-1.0.0.dev3-cp312-cp312-manylinux_2_5_x86_64.manylinux1_x86_64.whl:

Publisher: release.yml on stlmc/stlmc

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

File details

Details for the file stlmc-1.0.0.dev3-cp312-cp312-macosx_14_0_arm64.whl.

File metadata

File hashes

Hashes for stlmc-1.0.0.dev3-cp312-cp312-macosx_14_0_arm64.whl
Algorithm Hash digest
SHA256 9120895655433f6c57a0b14d5f761501d653d4c30dad9a08adfc9ec94529a8bd
MD5 945a8e8a91dad9d7070ba14d2c8dc872
BLAKE2b-256 00b666447748222ff7e3ab7a1dd0004c60f227e09e077576ced49e08cf7325a6

See more details on using hashes here.

Provenance

The following attestation bundles were made for stlmc-1.0.0.dev3-cp312-cp312-macosx_14_0_arm64.whl:

Publisher: release.yml on stlmc/stlmc

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

File details

Details for the file stlmc-1.0.0.dev3-cp311-cp311-manylinux_2_5_x86_64.manylinux1_x86_64.whl.

File metadata

File hashes

Hashes for stlmc-1.0.0.dev3-cp311-cp311-manylinux_2_5_x86_64.manylinux1_x86_64.whl
Algorithm Hash digest
SHA256 63709af6590e53636bf40baff781630e9c2395deeab52f20767a88bf6c4dab1e
MD5 cc42907a13d78e0ec18cb2771046500a
BLAKE2b-256 9bdeb5bc9f4d934c4461633f4214c506f257565928a32e92f31d6183e21775a2

See more details on using hashes here.

Provenance

The following attestation bundles were made for stlmc-1.0.0.dev3-cp311-cp311-manylinux_2_5_x86_64.manylinux1_x86_64.whl:

Publisher: release.yml on stlmc/stlmc

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

File details

Details for the file stlmc-1.0.0.dev3-cp311-cp311-macosx_14_0_arm64.whl.

File metadata

File hashes

Hashes for stlmc-1.0.0.dev3-cp311-cp311-macosx_14_0_arm64.whl
Algorithm Hash digest
SHA256 3ecc123d8689fb39d335699ccb2419d0ced169ed3be456ec95805c4f9d872a66
MD5 20a03c8781e933664e1c5418c92069f8
BLAKE2b-256 807b893b2f4e241d80aa6cb48e68850a13113334b3ac989f6959157e6c4c2e5b

See more details on using hashes here.

Provenance

The following attestation bundles were made for stlmc-1.0.0.dev3-cp311-cp311-macosx_14_0_arm64.whl:

Publisher: release.yml on stlmc/stlmc

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

File details

Details for the file stlmc-1.0.0.dev3-cp310-cp310-manylinux_2_5_x86_64.manylinux1_x86_64.whl.

File metadata

File hashes

Hashes for stlmc-1.0.0.dev3-cp310-cp310-manylinux_2_5_x86_64.manylinux1_x86_64.whl
Algorithm Hash digest
SHA256 3346e0faccb8d1014d315748a7a82524ff4c1dbbc19907f2961f48adcff8a3d5
MD5 562a539fff26334509a16a0210ee73b1
BLAKE2b-256 85092ed326c42ba934d6d492f424ae0f6c019bd6ca5708947930fc252e7673de

See more details on using hashes here.

Provenance

The following attestation bundles were made for stlmc-1.0.0.dev3-cp310-cp310-manylinux_2_5_x86_64.manylinux1_x86_64.whl:

Publisher: release.yml on stlmc/stlmc

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

File details

Details for the file stlmc-1.0.0.dev3-cp310-cp310-macosx_14_0_arm64.whl.

File metadata

File hashes

Hashes for stlmc-1.0.0.dev3-cp310-cp310-macosx_14_0_arm64.whl
Algorithm Hash digest
SHA256 95c8124e34a77bce7618148b52bf20f80c1c18e97b466d892e6502b9080c2793
MD5 8d288642adc731c6e5e00bb8c8f64038
BLAKE2b-256 34ed60981f7e0693445c027d6385b2a36bbad4d4a2b52972db1fbc0d15f34d7f

See more details on using hashes here.

Provenance

The following attestation bundles were made for stlmc-1.0.0.dev3-cp310-cp310-macosx_14_0_arm64.whl:

Publisher: release.yml on stlmc/stlmc

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

File details

Details for the file stlmc-1.0.0.dev3-cp39-cp39-manylinux_2_5_x86_64.manylinux1_x86_64.whl.

File metadata

File hashes

Hashes for stlmc-1.0.0.dev3-cp39-cp39-manylinux_2_5_x86_64.manylinux1_x86_64.whl
Algorithm Hash digest
SHA256 5f6d1166757c2d0854c78ab759252a86d8874a000ecc36f9fcf91a04fdf83f03
MD5 d6708433a85db0f18c50dc33f9235cfe
BLAKE2b-256 c801c124f21b3b828a6a0d06ec3bb0d01b055d1bab217310c1579997c37081f9

See more details on using hashes here.

Provenance

The following attestation bundles were made for stlmc-1.0.0.dev3-cp39-cp39-manylinux_2_5_x86_64.manylinux1_x86_64.whl:

Publisher: release.yml on stlmc/stlmc

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

File details

Details for the file stlmc-1.0.0.dev3-cp39-cp39-macosx_14_0_arm64.whl.

File metadata

File hashes

Hashes for stlmc-1.0.0.dev3-cp39-cp39-macosx_14_0_arm64.whl
Algorithm Hash digest
SHA256 19733860006fc529d27958d75f15f6e5a98a1046240fcb166f3ef25944c4ff11
MD5 b31701b0cfc2308fd50fbdd503380bcd
BLAKE2b-256 9894f343830435b8469b17b576f93557259d5363d19a9879b746fcfd489bfeff

See more details on using hashes here.

Provenance

The following attestation bundles were made for stlmc-1.0.0.dev3-cp39-cp39-macosx_14_0_arm64.whl:

Publisher: release.yml on stlmc/stlmc

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

File details

Details for the file stlmc-1.0.0.dev3-cp38-cp38-manylinux_2_5_x86_64.manylinux1_x86_64.whl.

File metadata

File hashes

Hashes for stlmc-1.0.0.dev3-cp38-cp38-manylinux_2_5_x86_64.manylinux1_x86_64.whl
Algorithm Hash digest
SHA256 0ed72c2a973750927350ae9960dbce27f4ebf72ec372143f4137844f2377f8d3
MD5 b12593f38ac584add831aec704ff3b94
BLAKE2b-256 e752e1c0dd6fe14fcd9882c6433dedde875d7b647f4a1460f7e923b0678d082b

See more details on using hashes here.

Provenance

The following attestation bundles were made for stlmc-1.0.0.dev3-cp38-cp38-manylinux_2_5_x86_64.manylinux1_x86_64.whl:

Publisher: release.yml on stlmc/stlmc

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

File details

Details for the file stlmc-1.0.0.dev3-cp38-cp38-macosx_14_0_arm64.whl.

File metadata

File hashes

Hashes for stlmc-1.0.0.dev3-cp38-cp38-macosx_14_0_arm64.whl
Algorithm Hash digest
SHA256 970d99a70eaa03aa15be29804470411a8e84a9d1e5cd0b4d77b117a44ab04e10
MD5 3635bcecc0f39466008e6ea545cd8dc1
BLAKE2b-256 f8fd3b6da00c8999b991878e153d3c8f38d23bb6b2d642b0c006f9d578c430e9

See more details on using hashes here.

Provenance

The following attestation bundles were made for stlmc-1.0.0.dev3-cp38-cp38-macosx_14_0_arm64.whl:

Publisher: release.yml on stlmc/stlmc

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

Supported by

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