PV3 ⊧ STMC: Statistical Model Checkercan verify any property expressible in PRISM against any system expresible in PRISMStatistical 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."
- Model checking
- Statistical model checking
Type of toolStatistical model checker
Expected inputProbabilistic model
Format:PRISM (.pm file)