PV3 STMC: Statistical Model Checkercan verify any property expressible in PRISM against any system expresible in PRISM

Statistical model checker. "[STMC can] statically verify any black-box probabilistic system that PRISM can simulate, against probabilistic bounds on any property that PRISM can evaluate over individual executions of the system."

Application domain/field

Type of tool

Statistical model checker

Expected input

Probabilistic model

Format:

PRISM (.pm file)

Expected output

? ("Result: true" or "Result: false"?)

Internals

Uses PRISM

Comments

License: GNU General Public License v3.0
Model checking Probabilistic

Links

Last commit date

13 January 2020

Related papers

https://doi.org/10.1007/978-3-030-53291-8_23 (CAV '20)

Last publication date

14 July 2020

Related tools

Other statistical model checkers: PRISM, MRMC, VESTA, YMER, COSMOS

ProVerB specific

View/edit source (Markdown)



ProVerB is a part of SLEBoK. Last updated: July 2022.