{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T03:20:34Z","timestamp":1779074434028,"version":"3.51.4"},"publisher-location":"Cham","reference-count":89,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030837228","type":"print"},{"value":"9783030837235","type":"electronic"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"DOI":"10.1007\/978-3-030-83723-5_15","type":"book-chapter","created":{"date-parts":[[2021,8,4]],"date-time":"2021-08-04T06:02:58Z","timestamp":1628056978000},"page":"216-241","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":37,"title":["On Correctness, Precision, and Performance in Quantitative Verification"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8807-1548","authenticated-orcid":false,"given":"Carlos E.","family":"Budde","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3268-8674","authenticated-orcid":false,"given":"Arnd","family":"Hartmanns","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6353-227X","authenticated-orcid":false,"given":"Michaela","family":"Klauck","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8122-2881","authenticated-orcid":false,"given":"Jan","family":"K\u0159et\u00ednsk\u00fd","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4137-8862","authenticated-orcid":false,"given":"David","family":"Parker","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2843-5511","authenticated-orcid":false,"given":"Tim","family":"Quatmann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4343-9323","authenticated-orcid":false,"given":"Andrea","family":"Turrini","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8269-9489","authenticated-orcid":false,"given":"Zhen","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,8,5]]},"reference":[{"key":"15_CR1","doi-asserted-by":"publisher","unstructured":"Abate, A., et al.: ARCH-COMP19 category report: stochastic modelling. In: ARCH. EPiC Series in Computing, vol. 61, pp. 62\u2013102. EasyChair (2019). https:\/\/doi.org\/10.29007\/f2vb","DOI":"10.29007\/f2vb"},{"key":"15_CR2","doi-asserted-by":"publisher","unstructured":"Agha, G., Palmskog, K.: A survey of statistical model checking. ACM Trans. Model. Comput. Simul. 28(1), 6:1\u20136:39 (2018). https:\/\/doi.org\/10.1145\/3158668","DOI":"10.1145\/3158668"},{"issue":"2","key":"15_CR3","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183\u2013235 (1994). https:\/\/doi.org\/10.1016\/0304-3975(94)90010-8","journal-title":"Theoret. Comput. Sci."},{"key":"15_CR4","doi-asserted-by":"publisher","unstructured":"Amparore, E.G., Balbo, G., Beccuti, M., Donatelli, S., Franceschinis, G.: 30 years of GreatSPN. In: Fiondella, L., Puliafito, A. (eds.) Principles of Performance and Reliability Modeling and Evaluation, pp. 227\u2013254. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-30599-8_9","DOI":"10.1007\/978-3-319-30599-8_9"},{"key":"15_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/978-3-642-40793-2_27","volume-title":"Computer Safety, Reliability, and Security","author":"F Arnold","year":"2013","unstructured":"Arnold, F., Belinfante, A., van der Berg, F., Guck, D., Stoelinga, M.: DFTCalc: a tool for efficient fault tree analysis. In: SAFECOMP. LNCS, vol. 8153, pp. 293\u2013301. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-40793-2_27"},{"key":"15_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/978-3-030-01090-4_19","volume-title":"Automated Technology for Verification and Analysis","author":"P Ashok","year":"2018","unstructured":"Ashok, P., Butkova, Y., Hermanns, H., Kret\u00ednsk\u00fd, J.: Continuous-time Markov decisions based on partial exploration. In: ATVA. LNCS, vol. 11138, pp. 317\u2013334. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-030-01090-4_19"},{"key":"15_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/978-3-319-63387-9_10","volume-title":"Computer Aided Verification","author":"P Ashok","year":"2017","unstructured":"Ashok, P., Chatterjee, K., Daca, P., Kret\u00ednsk\u00fd, J., Meggendorfer, T.: Value iteration for long-run average reward in Markov decision processes. In: CAV. LNCS, vol. 10426, pp. 201\u2013221. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_10"},{"key":"15_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"497","DOI":"10.1007\/978-3-030-25540-4_29","volume-title":"Computer Aided Verification","author":"P Ashok","year":"2019","unstructured":"Ashok, P., Kret\u00ednsk\u00fd, J., Weininger, M.: PAC statistical model checking for Markov decision processes and stochastic games. In: CAV. LNCS, vol. 11561, pp. 497\u2013519. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_29"},{"key":"15_CR9","doi-asserted-by":"publisher","first-page":"963","DOI":"10.1007\/978-3-319-10575-8_28","volume-title":"Handbook of Model Checking","author":"C Baier","year":"2018","unstructured":"Baier, C., de Alfaro, L., Forejt, V., Kwiatkowska, M.: Model checking probabilistic systems. In: Handbook of Model Checking, pp. 963\u2013999. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_28"},{"key":"15_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/3-540-48320-9_12","volume-title":"CONCUR\u201999 Concurrency Theory","author":"C Baier","year":"1999","unstructured":"Baier, C., Katoen, J.P., Hermanns, H.: Approximate symbolic model checking of continuous-time Markov chains. In: CONCUR. LNCS, vol. 1664, pp. 146\u2013161. Springer (1999). https:\/\/doi.org\/10.1007\/3-540-48320-9_12"},{"key":"15_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/978-3-319-63387-9_8","volume-title":"Computer Aided Verification","author":"C Baier","year":"2017","unstructured":"Baier, C., Klein, J., Leuschner, L., Parker, D., Wunderlich, S.: Ensuring the reliability of your model checker: interval iteration for MDPs. In: CAV. LNCS, vol. 10426, pp. 160\u2013180. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_8"},{"key":"15_CR12","doi-asserted-by":"publisher","unstructured":"Bauer, M.S., Mathur, U., Chadha, R., Sistla, A.P., Viswanathan, M.: Exact quantitative probabilistic model checking through rational search. In: FMCAD, pp. 92\u201399. IEEE (2017). https:\/\/doi.org\/10.23919\/FMCAD.2017.8102246","DOI":"10.23919\/FMCAD.2017.8102246"},{"key":"15_CR13","doi-asserted-by":"publisher","unstructured":"Behrmann, G., et al.: UPPAAL 4.0. In: QEST, pp. 125\u2013126. IEEE Computer Society (2006). https:\/\/doi.org\/10.1109\/QEST.2006.59","DOI":"10.1109\/QEST.2006.59"},{"key":"15_CR14","unstructured":"Bonet, B., Geffner, H.: Labeled RTDP: improving the convergence of real-time dynamic programming. In: ICAPS, pp. 12\u201321. AAAI Press (2003)"},{"key":"15_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/978-3-319-11936-6_8","volume-title":"Automated Technology for Verification and Analysis","author":"T Br\u00e1zdil","year":"2014","unstructured":"Br\u00e1zdil, T., Chatterjee, K., Chmelik, M., Forejt, V., Kret\u00ednsk\u00fd, J., Kwiatkowska, M.Z., Parker, D., Ujma, M.: Verification of Markov decision processes using learning algorithms. In: ATVA. LNCS, vol. 8837, pp. 98\u2013114. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-11936-6_8"},{"key":"15_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1007\/978-3-319-69483-2_3","volume-title":"Dependable Software Engineering. Theories, Tools, and Applications","author":"CE Budde","year":"2017","unstructured":"Budde, C.E., D\u2019Argenio, P.R., Hartmanns, A.: Better automated importance splitting for transient rare events. In: SETTA. LNCS, vol. 10606, pp. 42\u201358. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-69483-2_3"},{"key":"15_CR17","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1016\/j.scico.2019.01.006","volume":"174","author":"CE Budde","year":"2019","unstructured":"Budde, C.E., D\u2019Argenio, P.R., Hartmanns, A.: Automated compositional importance splitting. Sci. Comput. Program. 174, 90\u2013108 (2019). DOI: 10.1016\/j.scico.2019.01.006","journal-title":"Sci. Comput. Program."},{"key":"15_CR18","doi-asserted-by":"crossref","unstructured":"Budde, C.E., D\u2019Argenio, P.R., Hartmanns, A., Sedwards, S.: An efficient statistical model checker for nondeterminism and rare events. STTT (2020, to appear)","DOI":"10.1007\/s10009-020-00563-2"},{"key":"15_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-662-54580-5_9","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"CE Budde","year":"2017","unstructured":"Budde, C.E., Dehnert, C., Hahn, E.M., Hartmanns, A., Junges, S., Turrini, A.: JANI: Quantitative model and tool interaction. TACAS. LNCS 10206, 151\u2013168 (2017). https:\/\/doi.org\/10.1007\/978-3-662-54580-5_9"},{"key":"15_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/978-3-030-17465-1_11","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Y Butkova","year":"2019","unstructured":"Butkova, Y., Fox, G.: Optimal time-bounded reachability analysis for concurrent systems. In: TACAS. LNCS, vol. 11428, pp. 191\u2013208. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-17465-1_11"},{"key":"15_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/978-3-030-30281-8_4","volume-title":"Quantitative Evaluation of Systems","author":"Y Butkova","year":"2019","unstructured":"Butkova, Y., Hartmanns, A., Hermanns, H.: A Modest approach to modelling and checking Markov automata. In: QEST. LNCS, vol. 11785, pp. 52\u201369. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-30281-8_4"},{"key":"15_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1007\/978-3-319-24953-7_12","volume-title":"Automated Technology for Verification and Analysis","author":"Y Butkova","year":"2015","unstructured":"Butkova, Y., Hatefi, H., Hermanns, H., Krc\u00e1l, J.: Optimal continuous time Markov decisions. In: ATVA. LNCS, vol. 9364, pp. 166\u2013182. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-319-24953-7_12"},{"key":"15_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/978-3-662-54580-5_11","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Y Butkova","year":"2017","unstructured":"Butkova, Y., Wimmer, R., Hermanns, H.: Long-run rewards for Markov automata. TACAS. LNCS 10206, 188\u2013203 (2017). https:\/\/doi.org\/10.1007\/978-3-662-54580-5_11"},{"key":"15_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1007\/978-3-030-30942-8_8","volume-title":"Formal Methods \u2013 The Next 30 Years","author":"M \u010ce\u0161ka","year":"2019","unstructured":"Ceska, M., Hensel, C., Junges, S., Katoen, J.P.: Counterexample-driven synthesis for probabilistic program sketches. In: FM. LNCS, vol. 11800, pp. 101\u2013120. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-30942-8_8"},{"issue":"1","key":"15_CR25","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/s10703-013-0183-7","volume":"43","author":"T Chen","year":"2013","unstructured":"Chen, T., Forejt, V., Kwiatkowska, M.Z., Parker, D., Simaitis, A.: Automatic verification of competitive stochastic systems. Formal Methods Syst. Des. 43(1), 61\u201392 (2013). DOI: 10.1007\/s10703-013-0183-7","journal-title":"Formal Methods Syst. Des."},{"key":"15_CR26","doi-asserted-by":"publisher","unstructured":"Courtney, T., Gaonkar, S., Keefe, K., Rozier, E., Sanders, W.H.: M\u00f6bius 2.3: an extensible tool for dependability, security, and performance evaluation of large and complex system models. In: DSN, pp. 353\u2013358. IEEE Computer Society (2009). https:\/\/doi.org\/10.1109\/DSN.2009.5270318","DOI":"10.1109\/DSN.2009.5270318"},{"key":"15_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/978-3-319-33693-0_7","volume-title":"Integrated Formal Methods","author":"PR D\u2019Argenio","year":"2016","unstructured":"D\u2019Argenio, P.R., Hartmanns, A., Legay, A., Sedwards, S.: Statistical approximation of optimal schedulers for probabilistic timed automata. In: iFM. LNCS, vol. 9681, pp. 99\u2013114. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-33693-0_7"},{"key":"15_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"336","DOI":"10.1007\/978-3-030-03421-4_22","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Verification","author":"PR D\u2019Argenio","year":"2018","unstructured":"D\u2019Argenio, P.R., Hartmanns, A., Sedwards, S.: Lightweight statistical model checking in nondeterministic continuous time. In: ISoLA. LNCS, vol. 11245, pp. 336\u2013353. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-030-03421-4_22"},{"key":"15_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/3-540-45605-8_5","volume-title":"Process Algebra and Probabilistic Methods: Performance Modeling and Verification","author":"PR D\u2019Argenio","year":"2002","unstructured":"D\u2019Argenio, P.R., Jeannet, B., Jensen, H.E., Larsen, K.G.: Reduction and refinement strategies for probabilistic analysis. In: PAPM-PROBMIV. LNCS, vol. 2399, pp. 57\u201376. Springer (2002). https:\/\/doi.org\/10.1007\/3-540-45605-8_5"},{"key":"15_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/978-3-319-11936-6_11","volume-title":"Automated Technology for Verification and Analysis","author":"C Dehnert","year":"2014","unstructured":"Dehnert, C., Jansen, N., Wimmer, R., \u00c1brah\u00e1m, E., Katoen, J.P.: Fast debugging of PRISM models. In: ATVA. LNCS, vol. 8837, pp. 146\u2013162. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-11936-6_11"},{"key":"15_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1007\/978-3-319-21690-4_13","volume-title":"Computer Aided Verification","author":"C Dehnert","year":"2015","unstructured":"Dehnert, C., et al.: PROPhESY: A PRObabilistic ParamEter SYnthesis tool. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 214\u2013231. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_13"},{"key":"15_CR32","doi-asserted-by":"publisher","unstructured":"Dehnert, C., Junges, S., Katoen, J.P., Volk, M.: A Storm is coming: a modern probabilistic model checker. In: CAV. LNCS, vol. 10427, pp. 592\u2013600. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-63390-9_31","DOI":"10.1007\/978-3-319-63390-9_31"},{"key":"15_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1007\/978-3-030-45190-5_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"F Delgrange","year":"2020","unstructured":"Delgrange, F., Katoen, J.P., Quatmann, T., Randour, M.: Simple strategies in multi-objective MDPs. In: TACAS. LNCS, vol. 12078, pp. 346\u2013364. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-45190-5_19"},{"key":"15_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/978-3-319-25942-0_3","volume-title":"Dependable Software Engineering: Theories, Tools, and Applications","author":"T van Dijk","year":"2015","unstructured":"van Dijk, T., Hahn, E.M., Jansen, D.N., Li, Y., Neele, T., Stoelinga, M., Turrini, A., Zhang, L.: A comparative study of BDD packages for probabilistic symbolic model checking. In: SETTA. LNCS, vol. 9409, pp. 35\u201351. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-319-25942-0_3"},{"key":"15_CR35","doi-asserted-by":"publisher","unstructured":"Eisentraut, C., Hermanns, H., Zhang, L.: On probabilistic automata in continuous time. In: LICS, pp. 342\u2013351. IEEE Computer Society (2010). https:\/\/doi.org\/10.1109\/LICS.2010.41","DOI":"10.1109\/LICS.2010.41"},{"key":"15_CR36","doi-asserted-by":"publisher","unstructured":"Etessami, K., Kwiatkowska, M.Z., Vardi, M.Y., Yannakakis, M.: Multi-objective model checking of Markov decision processes. Logic. Methods Comput. Sci. 4(4) (2008). https:\/\/doi.org\/10.2168\/LMCS-4(4:8)2008","DOI":"10.2168\/LMCS-4(4:8)2008"},{"key":"15_CR37","doi-asserted-by":"publisher","unstructured":"Feng, Y., Hahn, E.M., Turrini, A., Ying, S.: Model checking omega-regular properties for quantum Markov chains. In: CONCUR. LIPIcs, vol. 85, pp. 35:1\u201335:16. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2017). https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2017.35","DOI":"10.4230\/LIPIcs.CONCUR.2017.35"},{"key":"15_CR38","doi-asserted-by":"publisher","unstructured":"Fu, C., Turrini, A., Huang, X., Song, L., Feng, Y., Zhang, L.: Model checking probabilistic epistemic logic for probabilistic multiagent systems. In: IJCAI, pp. 4757\u20134763. ijcai.org (2018). https:\/\/doi.org\/10.24963\/ijcai.2018\/661","DOI":"10.24963\/ijcai.2018\/661"},{"key":"15_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"300","DOI":"10.1007\/978-3-030-01090-4_18","volume-title":"Automated Technology for Verification and Analysis","author":"P Gainer","year":"2018","unstructured":"Gainer, P., Hahn, E.M., Schewe, S.: Accelerated model checking of parametric Markov chains. In: ATVA. LNCS, vol. 11138, pp. 300\u2013316. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-030-01090-4_18"},{"key":"15_CR40","doi-asserted-by":"publisher","unstructured":"Gordon, A.D., Henzinger, T.A., Nori, A.V., Rajamani, S.K.: Probabilistic programming. In: FOSE, pp. 167\u2013181. ACM (2014). https:\/\/doi.org\/10.1145\/2593882.2593900","DOI":"10.1145\/2593882.2593900"},{"key":"15_CR41","unstructured":"Gros, T.P.: Markov automata taken by Storm. Master\u2019s thesis, Saarland University, Germany (2018)"},{"key":"15_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/978-3-642-40196-1_5","volume-title":"Quantitative Evaluation of Systems","author":"D Guck","year":"2013","unstructured":"Guck, D., Hatefi, H., Hermanns, H., Katoen, J.P., Timmer, M.: Modelling, reduction and analysis of Markov automata. In: QEST. LNCS, vol. 8054, pp. 55\u201371. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-40196-1_5"},{"key":"15_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-3-319-11439-2_10","volume-title":"Reachability Problems","author":"S Haddad","year":"2014","unstructured":"Haddad, S., Monmege, B.: Reachability in MDPs: Refining convergence of value iteration. In: RP. LNCS, vol. 8762, pp. 125\u2013137. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-11439-2_10"},{"key":"15_CR44","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1016\/j.tcs.2016.12.003","volume":"735","author":"S Haddad","year":"2018","unstructured":"Haddad, S., Monmege, B.: Interval iteration algorithm for MDPs and IMDPs. Theor. Comput. Sci. 735, 111\u2013131 (2018). https:\/\/doi.org\/10.1016\/j.tcs.2016.12.003","journal-title":"Theoret. Comput. Sci."},{"key":"15_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/978-3-319-47677-3_6","volume-title":"Dependable Software Engineering: Theories, Tools, and Applications","author":"EM Hahn","year":"2016","unstructured":"Hahn, E.M., Hartmanns, A.: A comparison of time- and reward-bounded probabilistic model checking techniques. SETTA. LNCS 9984, 85\u2013100 (2016). https:\/\/doi.org\/10.1007\/978-3-319-47677-3_6"},{"key":"15_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/978-3-030-17502-3_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"EM Hahn","year":"2019","unstructured":"Hahn, E.M., Hartmanns, A., Hensel, C., Klauck, M., Klein, J., Kret\u00ednsk\u00fd, J., Parker, D., Quatmann, T., Ruijters, E., Steinmetz, M.: The 2019 comparison of tools for the analysis of quantitative formal models (QComp 2019 competition report). In: TACAS: TOOLympics. LNCS, vol. 11429, pp. 69\u201392. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-17502-3_5"},{"issue":"2","key":"15_CR47","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/s10703-012-0167-z","volume":"43","author":"EM Hahn","year":"2013","unstructured":"Hahn, E.M., Hartmanns, A., Hermanns, H., Katoen, J.P.: A compositional modelling and analysis framework for stochastic hybrid systems. Formal Methods Syst. Des. 43(2), 191\u2013232 (2013). DOI: 10.1007\/s10703-012-0167-z","journal-title":"Formal Methods Syst. Des."},{"key":"15_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/978-3-319-66335-7_13","volume-title":"Quantitative Evaluation of Systems","author":"EM Hahn","year":"2017","unstructured":"Hahn, E.M., Hashemi, V., Hermanns, H., Lahijanian, M., Turrini, A.: Multi-objective robust strategy synthesis for interval MDPs. In: QEST. LNCS, vol. 10503, pp. 207\u2013223. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-66335-7_13"},{"key":"15_CR49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/978-3-319-43425-4_4","volume-title":"Quantitative Evaluation of Systems","author":"EM Hahn","year":"2016","unstructured":"Hahn, Ernst Moritz, Hashemi, Vahid, Hermanns, Holger, Turrini, Andrea: Exploiting Robust Optimization for Interval Probabilistic Bisimulation. In: Agha, Gul, Van Houdt, Benny (eds.) QEST 2016. LNCS, vol. 9826, pp. 55\u201371. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-43425-4_4"},{"key":"15_CR50","unstructured":"Hahn, E.M., Li, G., Schewe, S., Zhang, L.: Lazy determinisation for quantitative model checking. CoRR abs\/1311.2928 (2013). arxiv.org\/abs\/1311.2928"},{"key":"15_CR51","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1007\/978-3-319-06410-9_22","volume-title":"FM 2014: Formal Methods","author":"EM Hahn","year":"2014","unstructured":"Hahn, E.M., Li, Y., Schewe, S., Turrini, A., Zhang, L.: iscasMc: a web-based probabilistic model checker. In: FM. LNCS, vol. 8442, pp. 312\u2013317. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-06410-9_22"},{"key":"15_CR52","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1007\/978-3-319-41540-6_16","volume-title":"Computer Aided Verification","author":"EM Hahn","year":"2016","unstructured":"Hahn, E.M., Schewe, S., Turrini, A., Zhang, L.: A simple algorithm for solving qualitative probabilistic parity games. In: CAV. LNCS, vol. 9780, pp. 291\u2013311. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-41540-6_16"},{"key":"15_CR53","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"593","DOI":"10.1007\/978-3-642-54862-8_51","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Hartmanns","year":"2014","unstructured":"Hartmanns, A., Hermanns, H.: The modest toolset: an integrated environment for quantitative modelling and verification. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 593\u2013598. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_51"},{"key":"15_CR54","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-319-24953-7_10","volume-title":"Automated Technology for Verification and Analysis","author":"A Hartmanns","year":"2015","unstructured":"Hartmanns, A., Hermanns, H.: Explicit model checking of very large MDP using partitioning and secondary storage. In: ATVA. LNCS, vol. 9364, pp. 131\u2013147. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-319-24953-7_10"},{"key":"15_CR55","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"320","DOI":"10.1007\/978-3-319-89963-3_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Hartmanns","year":"2018","unstructured":"Hartmanns, A., Junges, S., Katoen, J.P., Quatmann, T.: Multi-cost bounded reachability in MDP. In: TACAS. LNCS, vol. 10806, pp. 320\u2013339. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-89963-3_19"},{"key":"15_CR56","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"488","DOI":"10.1007\/978-3-030-53291-8_26","volume-title":"Computer Aided Verification","author":"A Hartmanns","year":"2020","unstructured":"Hartmanns, A., Kaminski, B.L.: Optimistic value iteration. In: CAV. LNCS, vol. 12225, pp. 488\u2013511. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-53291-8_26"},{"key":"15_CR57","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.3965313","author":"A Hartmanns","year":"2020","unstructured":"Hartmanns, A., Klauck, M.: The 2020 Comparison of Tools for the Analysis of Quantitative Formal Models: Results and Reproduction. Zenodo (2020). https:\/\/doi.org\/10.5281\/zenodo.3965313","journal-title":"Zenodo"},{"key":"15_CR58","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"344","DOI":"10.1007\/978-3-030-17462-0_20","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Hartmanns","year":"2019","unstructured":"Hartmanns, A., Klauck, M., Parker, D., Quatmann, T., Ruijters, E.: The quantitative verification benchmark set. In: TACAS. LNCS, vol. 11427, pp. 344\u2013350. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-17462-0_20"},{"key":"15_CR59","doi-asserted-by":"publisher","unstructured":"Hartmanns, A., Sedwards, S., D\u2019Argenio, P.R.: Efficient simulation-based verification of probabilistic timed automata. In: Winter Simulation Conference, pp. 1419\u20131430. IEEE (2017). https:\/\/doi.org\/10.1109\/WSC.2017.8247885","DOI":"10.1109\/WSC.2017.8247885"},{"key":"15_CR60","doi-asserted-by":"crossref","unstructured":"Hensel, C., Junges, S., Katoen, J.P., Quatmann, T., Volk, M.: The probabilistic model checker Storm. CoRR abs\/2002.07080 (2020). arxiv.org\/abs\/2002.07080","DOI":"10.1007\/s10009-021-00633-z"},{"key":"15_CR61","unstructured":"Jansen, D.N.: Understanding Fox and Glynn\u2019s \u201cComputing Poisson probabilities\u201d. CTIT technical report series (2011)"},{"key":"15_CR62","unstructured":"Junges, S., et al.: Parameter synthesis for Markov models. CoRR abs\/1903.07993 (2019). arxiv.org\/abs\/1903.07993"},{"key":"15_CR63","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"623","DOI":"10.1007\/978-3-319-96145-3_36","volume-title":"Computer Aided Verification","author":"E Kelmendi","year":"2018","unstructured":"Kelmendi, E., Kr\u00e4mer, J., Kret\u00ednsk\u00fd, J., Weininger, M.: Value iteration for simple stochastic games: Stopping criterion and learning algorithm. In: CAV. LNCS, vol. 10981, pp. 623\u2013642. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_36"},{"key":"15_CR64","doi-asserted-by":"crossref","unstructured":"Klauck, M., Steinmetz, M., Hoffmann, J., Hermanns, H.: Compiling probabilistic model checking into prob. planning. In: ICAPS, pp. 150\u2013154. AAAI Press (2018)","DOI":"10.1609\/icaps.v28i1.13887"},{"key":"15_CR65","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1613\/jair.1.11595","volume":"68","author":"M Klauck","year":"2020","unstructured":"Klauck, M., Steinmetz, M., Hoffmann, J., Hermanns, H.: Bridging the gap between probabilistic model checking and probabilistic planning: Survey, compilations, and empirical comparison. J. Artif. Intell. Res. 68, 247\u2013310 (2020). https:\/\/doi.org\/10.1613\/jair.1.11595","journal-title":"J. Artif. Intell. Res."},{"key":"15_CR66","doi-asserted-by":"crossref","unstructured":"Kolobov, A., Mausam, Weld, D.S., Geffner, H.: Heuristic search for generalized stochastic shortest path MDPs. In: ICAPS. AAAI Press (2011)","DOI":"10.1609\/icaps.v21i1.13452"},{"key":"15_CR67","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1007\/978-3-642-04368-0_17","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"M Kwiatkowska","year":"2009","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D.: Stochastic games for verification of probabilistic timed automata. In: FORMATS. LNCS, vol. 5813, pp. 212\u2013227. Springer (2009). https:\/\/doi.org\/10.1007\/978-3-642-04368-0_17"},{"key":"15_CR68","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.Z., Norman, G., Parker, D.: PRISM 4.0: Verification of probabilistic real-time systems. In: CAV. LNCS, vol. 6806, pp. 585\u2013591. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_47"},{"key":"15_CR69","doi-asserted-by":"publisher","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D.: The PRISM benchmark suite. In: QEST, pp. 203\u2013204. IEEE Computer Society (2012). https:\/\/doi.org\/10.1109\/QEST.2012.14","DOI":"10.1109\/QEST.2012.14"},{"issue":"1","key":"15_CR70","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/s10703-006-0005-2","volume":"29","author":"MZ Kwiatkowska","year":"2006","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D., Sproston, J.: Performance analysis of probabilistic timed automata using digital clocks. Formal Methods Syst. Des. 29(1), 33\u201378 (2006). DOI: 10.1007\/s10703-006-0005-2","journal-title":"Formal Methods Syst. Des."},{"issue":"1","key":"15_CR71","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/S0304-3975(01)00046-9","volume":"282","author":"MZ Kwiatkowska","year":"2002","unstructured":"Kwiatkowska, M.Z., Norman, G., Segala, R., Sproston, J.: Automatic verification of real-time systems with discrete probability distributions. Theor. Comput. Sci. 282(1), 101\u2013150 (2002). https:\/\/doi.org\/10.1016\/S0304-3975(01)00046-9","journal-title":"Theoret. Comput. Sci."},{"key":"15_CR72","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"350","DOI":"10.1007\/978-3-319-15201-1_23","volume-title":"Software Engineering and Formal Methods","author":"A Legay","year":"2015","unstructured":"Legay, A., Sedwards, S., Traonouez, L.M.: Scalable verification of Markov decision processes. In: WS-FMDS at SEFM. LNCS, vol. 8938, pp. 350\u2013362. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-15201-1_23"},{"issue":"1","key":"15_CR73","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1016\/0029-5493(84)90060-8","volume":"77","author":"E Lewis","year":"1984","unstructured":"Lewis, E., B\u00f6hm, F.: Monte Carlo simulation of Markov unreliability models. Nucl. Eng. Design 77(1), 49\u201362 (1984). https:\/\/doi.org\/10.1016\/0029-5493(84)90060-8","journal-title":"Nucl. Eng. Design"},{"key":"15_CR74","doi-asserted-by":"crossref","unstructured":"Li, Y., Liu, W., Turrini, A., Hahn, E.M., Zhang, L.: An efficient synthesis algorithm for parametric Markov chains against linear time properties. CoRR abs\/1605.04400 (2016)","DOI":"10.1007\/978-3-319-47677-3_18"},{"key":"15_CR75","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L.M., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: TACAS. LNCS, vol. 4963, pp. 337\u2013340. Springer (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"15_CR76","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"540","DOI":"10.1007\/978-3-030-25540-4_31","volume-title":"Computer Aided Verification","author":"T Neupane","year":"2019","unstructured":"Neupane, T., Myers, C.J., Madsen, C., Zheng, H., Zhang, Z.: STAMINA: stochastic approximate model-checker for infinite-state analysis. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 540\u2013549. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_31"},{"key":"15_CR77","series-title":"Computational Biology","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1007\/978-3-030-17297-8_12","volume-title":"Automated Reasoning for Systems Biology and Medicine","author":"T Neupane","year":"2019","unstructured":"Neupane, T., Zhang, Z., Madsen, C., Zheng, H., Myers, C.J.: Approximation techniques for stochastic analysis of biological systems. In: Automated Reasoning for Systems Biology and Medicine, Computational Biology, vol. 30, pp. 327\u2013348. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-17297-8_12"},{"key":"15_CR78","doi-asserted-by":"publisher","unstructured":"Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley Series in Probability and Statistics, Wiley (1994). https:\/\/doi.org\/10.1002\/9780470316887","DOI":"10.1002\/9780470316887"},{"key":"15_CR79","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/978-3-319-63387-9_7","volume-title":"Computer Aided Verification","author":"T Quatmann","year":"2017","unstructured":"Quatmann, T., Junges, S., Katoen, J.P.: Markov automata with multiple objectives. In: CAV. LNCS, vol. 10426, pp. 140\u2013159. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_7"},{"key":"15_CR80","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"643","DOI":"10.1007\/978-3-319-96145-3_37","volume-title":"Computer Aided Verification","author":"T Quatmann","year":"2018","unstructured":"Quatmann, T., Katoen, J.P.: Sound value iteration. In: CAV. LNCS, vol. 10981, pp. 643\u2013661. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_37"},{"key":"15_CR81","doi-asserted-by":"publisher","unstructured":"Reijsbergen, D., de Boer, P.T., Scheinhardt, W.R.W., Juneja, S.: Path-ZVA: general, efficient, and automated importance sampling for highly reliable Markovian systems. ACM Trans. Model. Comput. Simul. 28(3), 22:1\u201322:25 (2018). https:\/\/doi.org\/10.1145\/3161569","DOI":"10.1145\/3161569"},{"key":"15_CR82","doi-asserted-by":"publisher","unstructured":"Ruijters, E., et al.: FFORT: a benchmark suite for fault tree analysis. In: ESREL (2019). https:\/\/doi.org\/10.3850\/978-981-11-2724-3_0641-cd","DOI":"10.3850\/978-981-11-2724-3_0641-cd"},{"key":"15_CR83","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1016\/j.ress.2019.02.004","volume":"186","author":"E Ruijters","year":"2019","unstructured":"Ruijters, E., Reijsbergen, D., de Boer, P.T., Stoelinga, M.: Rare event simulation for dynamic fault trees. Reliab. Eng. Syst. Saf. 186, 220\u2013231 (2019). DOI: 10.1016\/j.ress.2019.02.004","journal-title":"Reliab. Eng. Syst. Saf."},{"key":"15_CR84","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"479","DOI":"10.1007\/978-3-030-31784-3_28","volume-title":"Automated Technology for Verification and Analysis","author":"J Spel","year":"2019","unstructured":"Spel, J., Junges, S., Katoen, J.P.: Are parametric Markov chains monotonic? In: ATVA. LNCS, vol. 11781, pp. 479\u2013496. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-31784-3_28"},{"key":"15_CR85","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1613\/jair.5153","volume":"57","author":"M Steinmetz","year":"2016","unstructured":"Steinmetz, M., Hoffmann, J., Buffet, O.: Goal probability analysis in probabilistic planning: Exploring and enhancing the state of the art. J. Artif. Intell. Res. 57, 229\u2013271 (2016). https:\/\/doi.org\/10.1613\/jair.5153","journal-title":"J. Artif. Intell. Res."},{"key":"15_CR86","doi-asserted-by":"publisher","unstructured":"Sullivan, K.J., Dugan, J.B., Coppit, D.: The Galileo fault tree analysis tool. In: FTCS, pp. 232\u2013235. IEEE Computer Society (1999). https:\/\/doi.org\/10.1109\/FTCS.1999.781056","DOI":"10.1109\/FTCS.1999.781056"},{"issue":"1","key":"15_CR87","doi-asserted-by":"publisher","first-page":"370","DOI":"10.1109\/TII.2017.2710316","volume":"14","author":"M Volk","year":"2018","unstructured":"Volk, M., Junges, S., Katoen, J.P.: Fast dynamic fault tree analysis by model checking techniques. IEEE Trans. Ind. Informatics 14(1), 370\u2013379 (2018). DOI: 10.1109\/TII.2017.2710316","journal-title":"IEEE Trans. Ind. Informatics"},{"key":"15_CR88","doi-asserted-by":"publisher","unstructured":"Younes, H.L.S., Kwiatkowska, M.Z., Norman, G., Parker, D.: Numerical vs. statistical probabilistic model checking. Int. J. Softw. Tools Technol. Transf. 8(3), 216\u2013228 (2006). https:\/\/doi.org\/10.1007\/s10009-005-0187-8","DOI":"10.1007\/s10009-005-0187-8"},{"key":"15_CR89","doi-asserted-by":"publisher","first-page":"851","DOI":"10.1613\/jair.1880","volume":"24","author":"HLS Younes","year":"2005","unstructured":"Younes, H.L.S., Littman, M.L., Weissman, D., Asmuth, J.: The first probabilistic track of the International Planning Competition. J. Artif. Intell. Res. 24, 851\u2013887 (2005). DOI: 10.1613\/jair.1880","journal-title":"J. Artif. Intell. Res."}],"container-title":["Lecture Notes in Computer Science","Leveraging Applications of Formal Methods, Verification and Validation: Tools and Trends"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-83723-5_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,6]],"date-time":"2023-01-06T12:51:40Z","timestamp":1673009500000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-83723-5_15"}},"subtitle":["QComp 2020 Competition Report"],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030837228","9783030837235"],"references-count":89,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-83723-5_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"5 August 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ISoLA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Leveraging Applications of Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Rhodes","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Greece","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":"20 October 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 October 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"isola2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/isola-conference.org\/isola2020\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}