{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T07:59:51Z","timestamp":1743148791652,"version":"3.40.3"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030532901"},{"type":"electronic","value":"9783030532918"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2020,7,14]],"date-time":"2020-07-14T00:00:00Z","timestamp":1594684800000},"content-version":"vor","delay-in-days":195,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-53291-8_23","type":"book-chapter","created":{"date-parts":[[2020,7,15]],"date-time":"2020-07-15T20:03:35Z","timestamp":1594843415000},"page":"448-460","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["STMC: Statistical Model Checker with Stratified and Antithetic Sampling"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2025-0528","authenticated-orcid":false,"given":"Nima","family":"Roohi","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0431-1039","authenticated-orcid":false,"given":"Yu","family":"Wang","sequence":"additional","affiliation":[]},{"given":"Matthew","family":"West","sequence":"additional","affiliation":[]},{"given":"Geir E.","family":"Dullerud","sequence":"additional","affiliation":[]},{"given":"Mahesh","family":"Viswanathan","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,7,14]]},"reference":[{"issue":"1","key":"23_CR1","doi-asserted-by":"publisher","first-page":"6:1","DOI":"10.1145\/3158668","volume":"28","author":"G Agha","year":"2018","unstructured":"Agha, G., Palmskog, K.: A survey of statistical model checking. ACM Trans. Model. Comput. Simul. 28(1), 6:1\u20136:39 (2018)","journal-title":"ACM Trans. Model. Comput. Simul."},{"doi-asserted-by":"crossref","unstructured":"Ballarini, P., Djafri, H., Duflot, M., Haddad, S., Pekergin, N.: COSMOS: a statistical model checker for the hybrid automata stochastic logic. In: 2011 Eighth International Conference on Quantitative Evaluation of SysTems, pp. 143\u2013144 (2011)","key":"23_CR2","DOI":"10.1109\/QEST.2011.24"},{"unstructured":"Barbot, B., B\u00e9rard, B., Duplouy, Y., Haddad, S.: Statistical Model-Checking for Autonomous Vehicle Safety Validation. In: SIA Simulation Num\u00e9rique. Soci\u00e9t\u00e9 des Ing\u00e9nieurs de l\u2019Automobile (2017)","key":"23_CR3"},{"key":"23_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1007\/978-3-642-10373-5_17","volume-title":"Formal Methods and Software Engineering","author":"S Basu","year":"2009","unstructured":"Basu, S., Ghosh, A.P., He, R.: Approximate model checking of PCTL involving unbounded path properties. In: Breitman, K., Cavalcanti, A. (eds.) ICFEM 2009. LNCS, vol. 5885, pp. 326\u2013346. Springer, Heidelberg (2009). \nhttps:\/\/doi.org\/10.1007\/978-3-642-10373-5_17"},{"doi-asserted-by":"crossref","unstructured":"Bauer, M.S., Mathur, U., Chadha, R., Sistla, A.P., Viswanathan, M.: Exact quantitative probabilistic model checking through rational search. In: Proceedings of the 17th Conference on Formal Methods in Computer-Aided Design, FMCAD 2017, pp. 92\u201399. FMCAD Inc., Austin (2017)","key":"23_CR5","DOI":"10.23919\/FMCAD.2017.8102246"},{"key":"23_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"388","DOI":"10.1007\/978-3-642-34026-0_29","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change","author":"A David","year":"2012","unstructured":"David, A., Larsen, K.G., Legay, A., Miku\u010dionis, M., Poulsen, D.B., Sedwards, S.: Runtime verification of biological systems. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012. LNCS, vol. 7609, pp. 388\u2013404. Springer, Heidelberg (2012). \nhttps:\/\/doi.org\/10.1007\/978-3-642-34026-0_29"},{"issue":"1","key":"23_CR7","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1214\/aos\/996986505","volume":"29","author":"J Fan","year":"2001","unstructured":"Fan, J., Zhang, C., Zhang, J.: Generalized likelihood ratio statistics and Wilks phenomenon. Ann. Stat. 29(1), 153\u2013193 (2001)","journal-title":"Ann. Stat."},{"unstructured":"Hermanns, H., Meyer-Kayser, J., Siegle, M.: Multi terminal binary decision diagrams to represent and analyse continuous time Markov chains. In: Plateau, B., Stewart, W., Silva, M. (eds.) Proceedings of the 3rd International Workshop on Numerical Solution of Markov Chains (NSMC 1999), pp. 188\u2013207. Prensas Universitarias de Zaragoza (1999)","key":"23_CR8"},{"key":"23_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"498","DOI":"10.1007\/978-3-642-28756-5_37","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C Jegourel","year":"2012","unstructured":"Jegourel, C., Legay, A., Sedwards, S.: A platform for high performance statistical model checking \u2013 PLASMA. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 498\u2013503. Springer, Heidelberg (2012). \nhttps:\/\/doi.org\/10.1007\/978-3-642-28756-5_37"},{"doi-asserted-by":"crossref","unstructured":"Katoen, J., Khattri, M., Zapreevt, I.S.: A Markov reward model checker. In: Second International Conference on the Quantitative Evaluation of Systems (QEST 2005), pp. 243\u2013244 (2005)","key":"23_CR10","DOI":"10.1109\/QEST.2005.2"},{"issue":"11","key":"23_CR11","doi-asserted-by":"publisher","first-page":"1427","DOI":"10.1016\/j.conengprac.2006.07.003","volume":"15","author":"M Kwiatkowska","year":"2006","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Controller dependability analysis by probabilistic model checking. Control. Eng. Pract. 15(11), 1427\u20131434 (2006)","journal-title":"Control. Eng. Pract."},{"key":"23_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"M Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585\u2013591. Springer, Heidelberg (2011). \nhttps:\/\/doi.org\/10.1007\/978-3-642-22110-1_47"},{"issue":"2","key":"23_CR13","first-page":"303","volume":"11","author":"TL Lai","year":"2001","unstructured":"Lai, T.L.: Sequential Analysis: Some Classical Problems and New Challenges. Statistica Sinica 11(2), 303\u2013351 (2001)","journal-title":"Statistica Sinica"},{"key":"23_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-47166-2_1","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques","author":"KG Larsen","year":"2016","unstructured":"Larsen, K.G., Legay, A.: Statistical model checking: past, present, and future. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9952, pp. 3\u201315. Springer, Cham (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-319-47166-2_1"},{"key":"23_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/978-3-642-16612-9_11","volume-title":"Runtime Verification","author":"A Legay","year":"2010","unstructured":"Legay, A., Delahaye, B., Bensalem, S.: Statistical model checking: an overview. In: Barringer, H., Falcone, Y., Finkbeiner, B., Havelund, K., Lee, I., Pace, G., Ro\u015fu, G., Sokolsky, O., Tillmann, N. (eds.) RV 2010. LNCS, vol. 6418, pp. 122\u2013135. Springer, Heidelberg (2010). \nhttps:\/\/doi.org\/10.1007\/978-3-642-16612-9_11"},{"issue":"2","key":"23_CR16","first-page":"9","volume":"1","author":"J Muppala","year":"1994","unstructured":"Muppala, J., Ciardo, G., Trivedi, K.: Stochastic reward nets for reliability prediction. Commun. Reliab. Maint. Serv. 1(2), 9\u201320 (1994)","journal-title":"Commun. Reliab. Maint. Serv."},{"issue":"10","key":"23_CR17","doi-asserted-by":"publisher","first-page":"1629","DOI":"10.1109\/TCAD.2005.852033","volume":"24","author":"G Norman","year":"2005","unstructured":"Norman, G., Parker, D., Kwiatkowska, M., Shukla, S.: Evaluating the reliability of NAND multiplexing with PRISM. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 24(10), 1629\u20131637 (2005)","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circuits Syst."},{"doi-asserted-by":"crossref","unstructured":"Roohi, N., Wang, Y., West, M., Dullerud, G.E., Viswanathan, M.: Statistical verification of the Toyota powertrain control verification benchmark. In: 20th ACM International Conference on Hybrid Systems: Computation and Control (HSCC), pp. 65\u201370. ACM (2017)","key":"23_CR18","DOI":"10.1145\/3049797.3049804"},{"doi-asserted-by":"crossref","unstructured":"Sen, K., Viswanathan, M., Agha, G.: VESTA: A statistical model-checker and analyzer for probabilistic systems. In: Second International Conference on the Quantitative Evaluation of Systems, pp. 251\u2013252 (2005)","key":"23_CR19","DOI":"10.1109\/QEST.2005.42"},{"issue":"2","key":"23_CR20","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1214\/aoms\/1177731118","volume":"16","author":"A Wald","year":"1945","unstructured":"Wald, A.: Sequential tests of statistical hypotheses. Ann. Math. Stat. 16(2), 117\u2013186 (1945)","journal-title":"Ann. Math. Stat."},{"doi-asserted-by":"crossref","unstructured":"Wang, Y., Roohi, N., West, M., Viswanathan, M., Dullerud, G.: A Mori-Zwanzig and MITL based approach to statistical verification of continuous-time dynamical systems. In: International Federation of Automatic Control (IFAC PapersOnLine), vol. 48, no. 27, pp. 267\u2013273 (2015)","key":"23_CR21","DOI":"10.1016\/j.ifacol.2015.11.186"},{"doi-asserted-by":"crossref","unstructured":"Wang, Y., Roohi, N., West, M., Viswanathan, M., Dullerud, G.: Statistical verification of dynamical systems using set oriented methods. In: Hybrid Systems: Computation and Control (HSCC), pp. 169\u2013178 (2015)","key":"23_CR22","DOI":"10.1145\/2728606.2728627"},{"doi-asserted-by":"crossref","unstructured":"Wang, Y., Roohi, N., West, M., Viswanathan, M., Dullerud, G.: Verifying continuous-time stochastic hybrid systems via Mori-Zwanzig model reduction. In: 2016 IEEE 55th Conference on Decision and Control (CDC), pp. 3012\u20133017 (2016)","key":"23_CR23","DOI":"10.1109\/CDC.2016.7798719"},{"key":"23_CR24","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1007\/s10703-019-00339-8","volume":"54","author":"Y Wang","year":"2019","unstructured":"Wang, Y., Roohi, N., West, M., Viswanathan, M., Dullerud, G.E.: Statistical Verification of PCTL Using Antithetic and Stratified Samples. Form. Methods Syst. Des. 54, 145\u2013163 (2019). \nhttps:\/\/doi.org\/10.1007\/s10703-019-00339-8","journal-title":"Form. Methods Syst. Des."},{"doi-asserted-by":"crossref","unstructured":"Wang, Y., Roohi, N., West, M., Viswanathan, M., Dullerud, G.E.: Statistical verification of PCTL using stratified samples. In: 6th IFAC Conference on Analysis and Design of Hybrid Systems (ADHS), IFAC-PapersOnLine, vol. 51, pp. 85\u201390 (2018)","key":"23_CR25","DOI":"10.1016\/j.ifacol.2018.08.015"},{"issue":"3","key":"23_CR26","doi-asserted-by":"publisher","first-page":"419","DOI":"10.1080\/00401706.1962.10490022","volume":"4","author":"BP Welford","year":"1962","unstructured":"Welford, B.P.: Note on a method for calculating corrected sums of squares and products. Technometrics 4(3), 419\u2013420 (1962)","journal-title":"Technometrics"},{"key":"23_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"429","DOI":"10.1007\/11513988_43","volume-title":"Computer Aided Verification","author":"HLS Younes","year":"2005","unstructured":"Younes, H.L.S.: Ymer: a statistical model checker. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 429\u2013433. Springer, Heidelberg (2005). \nhttps:\/\/doi.org\/10.1007\/11513988_43"},{"key":"23_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/11609773_10","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"HLS Younes","year":"2005","unstructured":"Younes, H.L.S.: Error control for probabilistic model checking. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 142\u2013156. Springer, Heidelberg (2005). \nhttps:\/\/doi.org\/10.1007\/11609773_10"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-53291-8_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,7,15]],"date-time":"2020-07-15T20:06:54Z","timestamp":1594843614000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-53291-8_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030532901","9783030532918"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-53291-8_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"14 July 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Los Angeles, CA","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 July 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 July 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"32","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2020\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair.org","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"240","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"43","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"22","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"18% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference was held virtually due to the COVID-19 pandemic.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}