TY - GEN
T1 - STMC
T2 - 32nd International Conference on Computer Aided Verification, CAV 2020
AU - Roohi, Nima
AU - Wang, Yu
AU - West, Matthew
AU - Dullerud, Geir E.
AU - Viswanathan, Mahesh
N1 - Publisher Copyright:
© 2020, The Author(s).
PY - 2020
Y1 - 2020
N2 - is a statistical model checker that uses antithetic and stratified sampling techniques to reduce the number of samples and, hence, the amount of time required before making a decision. The tool is capable of statistically verifying any black-box probabilistic system thatcan simulate, against probabilistic bounds on any property thatcan evaluate over individual executions of the system. We have evaluated our tool on many examples and compared it with both symbolic and statistical algorithms. When the number of strata is large, our algorithms reduced the number of samples more than 3 times on average. Furthermore, being a statistical model checker makesable to verify models that are well beyond the reach of current symbolic model checkers. On large systems (up to states)was able to check 100% of benchmark systems, compared to existing symbolic methods in, which only succeeded on 13% of systems. The tool, installation instructions, benchmarks, and scripts for running the benchmarks are all available online as open source.
AB - is a statistical model checker that uses antithetic and stratified sampling techniques to reduce the number of samples and, hence, the amount of time required before making a decision. The tool is capable of statistically verifying any black-box probabilistic system thatcan simulate, against probabilistic bounds on any property thatcan evaluate over individual executions of the system. We have evaluated our tool on many examples and compared it with both symbolic and statistical algorithms. When the number of strata is large, our algorithms reduced the number of samples more than 3 times on average. Furthermore, being a statistical model checker makesable to verify models that are well beyond the reach of current symbolic model checkers. On large systems (up to states)was able to check 100% of benchmark systems, compared to existing symbolic methods in, which only succeeded on 13% of systems. The tool, installation instructions, benchmarks, and scripts for running the benchmarks are all available online as open source.
UR - http://www.scopus.com/inward/record.url?scp=85089218977&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85089218977&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-53291-8_23
DO - 10.1007/978-3-030-53291-8_23
M3 - Conference contribution
AN - SCOPUS:85089218977
SN - 9783030532901
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 448
EP - 460
BT - Computer Aided Verification - 32nd International Conference, CAV 2020, Proceedings
A2 - Lahiri, Shuvendu K.
A2 - Wang, Chao
PB - Springer
Y2 - 21 July 2020 through 24 July 2020
ER -