{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T02:50:10Z","timestamp":1784775010007,"version":"3.55.0"},"publisher-location":"Cham","reference-count":74,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030309411","type":"print"},{"value":"9783030309428","type":"electronic"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-30942-8_8","type":"book-chapter","created":{"date-parts":[[2019,9,22]],"date-time":"2019-09-22T23:03:06Z","timestamp":1569193386000},"page":"101-120","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":19,"title":["Counterexample-Driven Synthesis for Probabilistic Program Sketches"],"prefix":"10.1007","author":[{"given":"Milan","family":"\u010ce\u0161ka","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Christian","family":"Hensel","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sebastian","family":"Junges","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2019,9,23]]},"reference":[{"key":"8_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"270","DOI":"10.1007\/978-3-319-96145-3_15","volume-title":"Computer Aided Verification","author":"A Abate","year":"2018","unstructured":"Abate, A., David, C., Kesseli, P., Kroening, D., Polgreen, E.: Counterexample guided inductive synthesis modulo theories. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 270\u2013288. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_15"},{"key":"8_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1007\/978-3-319-07317-0_3","volume-title":"Formal Methods for Executable Software Models","author":"E \u00c1brah\u00e1m","year":"2014","unstructured":"\u00c1brah\u00e1m, E., Becker, B., Dehnert, C., Jansen, N., Katoen, J.-P., Wimmer, R.: Counterexample generation for discrete-time Markov models: an introductory survey. In: Bernardo, M., Damiani, F., H\u00e4hnle, R., Johnsen, E.B., Schaefer, I. (eds.) SFM 2014. LNCS, vol. 8483, pp. 65\u2013121. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-07317-0_3"},{"key":"8_CR3","unstructured":"Alur, R., et al.: Syntax-guided synthesis. In: Dependable Software Systems Engineering, NATO Science for Peace and Security Series, vol. 40, pp. 1\u201325. IOS Press (2015)"},{"issue":"12","key":"8_CR4","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1145\/3208071","volume":"61","author":"R Alur","year":"2018","unstructured":"Alur, R., Singh, R., Fisman, D., Solar-Lezama, A.: Search-based program synthesis. Commun. ACM 61(12), 84\u201393 (2018)","journal-title":"Commun. ACM"},{"key":"8_CR5","first-page":"94","volume":"95","author":"A Antonik","year":"2008","unstructured":"Antonik, A., Huth, M., Larsen, K.G., Nyman, U., Wasowski, A.: 20 years of modal and mixed specifications. Bull. EATCS 95, 94\u2013129 (2008)","journal-title":"Bull. EATCS"},{"key":"8_CR6","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. Handbook of Model Checking, pp. 963\u2013999. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_28"},{"key":"8_CR7","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"issue":"5","key":"8_CR8","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1109\/TSE.2004.9","volume":"30","author":"S Balsamo","year":"2004","unstructured":"Balsamo, S., Di Marco, A., Inverardi, P., Simeoni, M.: Model-based performance prediction in software development: a survey. IEEE Trans. Softw. Eng. 30(5), 295\u2013310 (2004)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"8_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1007\/978-3-642-19835-9_30","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Bartocci","year":"2011","unstructured":"Bartocci, E., Grosu, R., Katsaros, P., Ramakrishnan, C.R., Smolka, S.A.: Model repair for probabilistic systems. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 326\u2013340. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-19835-9_30"},{"issue":"1","key":"8_CR10","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.jss.2008.03.066","volume":"82","author":"S Becker","year":"2009","unstructured":"Becker, S., Koziolek, H., Reussner, R.: The Palladio component model for model-driven performance prediction. J. Syst. Softw. 82(1), 3\u201322 (2009)","journal-title":"J. Syst. Softw."},{"issue":"2\u20133","key":"8_CR11","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/s00236-015-0215-4","volume":"52","author":"N Benes","year":"2015","unstructured":"Benes, N., Kret\u00ednsk\u00fd, J., Larsen, K.G., M\u00f8ller, M.H., Sickert, S., Srba, J.: Refinement checking on parametric modal transition systems. Acta Inf. 52(2\u20133), 269\u2013297 (2015)","journal-title":"Acta Inf."},{"key":"8_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/978-3-642-28717-6_12","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"N Bene\u0161","year":"2012","unstructured":"Bene\u0161, N., K\u0159et\u00ednsk\u00fd, J., Guldstrand Larsen, K., M\u00f8ller, M.H., Srba, J.: Dual-priced modal transition systems with time durations. In: Bj\u00f8rner, N., Voronkov, A. (eds.) LPAR 2012. LNCS, vol. 7180, pp. 122\u2013137. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28717-6_12"},{"issue":"3","key":"8_CR13","first-page":"299","volume":"8","author":"L Benini","year":"2000","unstructured":"Benini, L., Bogliolo, A., Paleologo, G., Micheli, G.D.: Policy optimization for dynamic power management. IEEE Trans. CAD Integr. Circ. Syst. 8(3), 299\u2013316 (2000)","journal-title":"IEEE Trans. CAD Integr. Circ. Syst."},{"key":"8_CR14","unstructured":"Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press (2009)"},{"issue":"10","key":"8_CR15","doi-asserted-by":"publisher","first-page":"812","DOI":"10.1109\/TSE.2006.104","volume":"32","author":"HC Bohnenkamp","year":"2006","unstructured":"Bohnenkamp, H.C., D\u2019Argenio, P.R., Hermanns, H., Katoen, J.P.: MODEST: a compositional modeling formalism for hard and softly timed systems. IEEE Trans. Softw. Eng. 32(10), 812\u2013830 (2006)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"8_CR16","volume-title":"Foundations of Software and System Performance Engineering","author":"AB Bondy","year":"2014","unstructured":"Bondy, A.B.: Foundations of Software and System Performance Engineering. Addison Wesley, Boston (2014)"},{"key":"8_CR17","doi-asserted-by":"crossref","unstructured":"Bornholt, J., Torlak, E., Grossman, D., Ceze, L.: Optimizing synthesis with metasketches. In: POPL, pp. 775\u2013788. ACM (2016)","DOI":"10.1145\/2914770.2837666"},{"key":"8_CR18","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. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10206, pp. 151\u2013168. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54580-5_9"},{"issue":"1","key":"8_CR19","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1109\/TR.2015.2452931","volume":"65","author":"R Calinescu","year":"2016","unstructured":"Calinescu, R., Ghezzi, C., Johnson, K., et al.: Formal verification with confidence intervals to establish quality of service properties of software systems. IEEE Trans. Reliab. 65(1), 107\u2013125 (2016)","journal-title":"IEEE Trans. Reliab."},{"issue":"9","key":"8_CR20","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1145\/2330667.2330686","volume":"55","author":"R Calinescu","year":"2012","unstructured":"Calinescu, R., Ghezzi, C., Kwiatkowska, M.Z., Mirandola, R.: Self-adaptive software needs quantitative verification at runtime. Commun. ACM 55(9), 69\u201377 (2012)","journal-title":"Commun. ACM"},{"key":"8_CR21","doi-asserted-by":"crossref","unstructured":"Calinescu, R., \u010ce\u0161ka, M., Gerasimou, S., Kwiatkowska, M., Paoletti, N.: Designing robust software systems through parametric Markov chain synthesis. In: ICSA, pp. 131\u2013140. IEEE (2017)","DOI":"10.1109\/ICSA.2017.16"},{"key":"8_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"304","DOI":"10.1007\/978-3-319-66335-7_20","volume-title":"Quantitative Evaluation of Systems","author":"R Calinescu","year":"2017","unstructured":"Calinescu, R., \u010ce\u0161ka, M., Gerasimou, S., Kwiatkowska, M., Paoletti, N.: RODES: a robust-design synthesis tool for\u00a0probabilistic systems. In: Bertrand, N., Bortolussi, L. (eds.) QEST 2017. LNCS, vol. 10503, pp. 304\u2013308. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66335-7_20"},{"key":"8_CR23","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1016\/j.jss.2018.05.013","volume":"143","author":"R Calinescu","year":"2018","unstructured":"Calinescu, R., \u010ce\u0161ka, M., Gerasimou, S., Kwiatkowska, M., Paoletti, N.: Efficient synthesis of robust models for stochastic systems. J. Syst. Softw. 143, 140\u2013158 (2018)","journal-title":"J. Syst. Softw."},{"key":"8_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1007\/978-3-319-63390-9_20","volume-title":"Computer Aided Verification","author":"L Cardelli","year":"2017","unstructured":"Cardelli, L., et al.: Syntax-guided optimal synthesis for chemical reaction networks. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 375\u2013395. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63390-9_20"},{"key":"8_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-642-22110-1_20","volume-title":"Computer Aided Verification","author":"P \u010cern\u00fd","year":"2011","unstructured":"\u010cern\u00fd, P., Chatterjee, K., Henzinger, T.A., Radhakrishna, A., Singh, R.: Quantitative synthesis for concurrent programs. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 243\u2013259. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_20"},{"issue":"6","key":"8_CR26","doi-asserted-by":"publisher","first-page":"589","DOI":"10.1007\/s00236-016-0265-2","volume":"54","author":"M \u010ce\u0161ka","year":"2017","unstructured":"\u010ce\u0161ka, M., Dannenberg, F., Paoletti, N., Kwiatkowska, M., Brim, L.: Precise parameter synthesis for stochastic biochemical systems. Acta Inf. 54(6), 589\u2013623 (2017)","journal-title":"Acta Inf."},{"key":"8_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/978-3-030-17465-1_10","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M \u010ce\u0161ka","year":"2019","unstructured":"\u010ce\u0161ka, M., Jansen, N., Junges, S., Katoen, J.-P.: Shepherding hordes of Markov chains. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11428, pp. 172\u2013190. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17465-1_10"},{"issue":"1","key":"8_CR28","doi-asserted-by":"publisher","first-page":"1:1","DOI":"10.1145\/1838552.1838553","volume":"12","author":"R Chadha","year":"2010","unstructured":"Chadha, R., Viswanathan, M.: A counterexample-guided abstraction-refinement framework for markov decision processes. ACM Trans. Comput. Log. 12(1), 1:1\u20131:49 (2010)","journal-title":"ACM Trans. Comput. Log."},{"key":"8_CR29","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Chmelik, M., Davies, J.: A symbolic SAT-based algorithm for almost-sure reachability with small strategies in POMDPs. In: AAAI, pp. 3225\u20133232. AAAI Press (2016)","DOI":"10.1016\/j.artint.2016.01.007"},{"key":"8_CR30","doi-asserted-by":"crossref","unstructured":"Chaudhuri, S., Clochard, M., Solar-Lezama, A.: Bridging boolean and quantitative synthesis using smoothed proof search. In: POPL. ACM (2014)","DOI":"10.1145\/2535838.2535859"},{"key":"8_CR31","doi-asserted-by":"crossref","unstructured":"Chen, T., Hahn, E.M., Han, T., Kwiatkowska, M.Z., Qu, H., Zhang, L.: Model repair for Markov decision processes. In: TASE, pp. 85\u201392. IEEE (2013)","DOI":"10.1109\/TASE.2013.20"},{"issue":"1","key":"8_CR32","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/s00165-017-0432-4","volume":"30","author":"P Chrszon","year":"2018","unstructured":"Chrszon, P., Dubslaff, C., Kl\u00fcppelholz, S., Baier, C.: ProFeat: feature-oriented engineering for family-based probabilistic model checking. Formal Aspects Comput. 30(1), 45\u201375 (2018)","journal-title":"Formal Aspects Comput."},{"key":"8_CR33","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: Cassez, F., Raskin, J.-F. (eds.) ATVA 2014. LNCS, vol. 8837, pp. 146\u2013162. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-11936-6_11"},{"key":"8_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"592","DOI":"10.1007\/978-3-319-63390-9_31","volume-title":"Computer Aided Verification","author":"C Dehnert","year":"2017","unstructured":"Dehnert, C., Junges, S., Katoen, J.-P., Volk, M.: A storm is coming: a modern probabilistic model checker. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 592\u2013600. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63390-9_31"},{"key":"8_CR35","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1016\/j.ic.2013.10.002","volume":"232","author":"B Delahaye","year":"2013","unstructured":"Delahaye, B., et al.: Abstract probabilistic automata. Inf. Comput. 232, 66\u2013116 (2013)","journal-title":"Inf. Comput."},{"key":"8_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1007\/978-3-319-89960-2_17","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Dureja","year":"2018","unstructured":"Dureja, R., Rozier, K.Y.: More scalable LTL model checking via discovering design-space dependencies ($$D^{3}$$). In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10805, pp. 309\u2013327. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89960-2_17"},{"issue":"1","key":"8_CR37","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1109\/TSE.2015.2421318","volume":"42","author":"A Filieri","year":"2016","unstructured":"Filieri, A., Tamburrelli, G., Ghezzi, C.: Supporting self-adaptation via quantitative verification and sensitivity analysis at run time. IEEE Trans. Softw. Eng. 42(1), 75\u201399 (2016)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"8_CR38","series-title":"Springer Series in Reliability Engineering","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-30599-8","volume-title":"Principles of Performance and Reliability Modeling and Evaluation","year":"2016","unstructured":"Fiondella, L., Puliafito, A. (eds.): Principles of Performance and Reliability Modeling and Evaluation. SSRE. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-30599-8"},{"key":"8_CR39","doi-asserted-by":"crossref","unstructured":"Gerasimou, S., Tamburrelli, G., Calinescu, R.: Search-based synthesis of probabilistic models for quality-of-service software engineering. In: ASE, pp. 319\u2013330. IEEE Computer Society (2015)","DOI":"10.1109\/ASE.2015.22"},{"issue":"3","key":"8_CR40","doi-asserted-by":"publisher","first-page":"508","DOI":"10.1016\/j.infsof.2012.07.017","volume":"55","author":"C Ghezzi","year":"2013","unstructured":"Ghezzi, C., Sharifloo, A.M.: Model-based verification of quantitative non-functional properties for software product lines. Inf. Softw. Technol. 55(3), 508\u2013524 (2013)","journal-title":"Inf. Softw. Technol."},{"issue":"1\u20132","key":"8_CR41","first-page":"1","volume":"4","author":"S Gulwani","year":"2017","unstructured":"Gulwani, S., Polozov, O., Singh, R.: Program synthesis. Found. Trends Programm. Lang. 4(1\u20132), 1\u2013119 (2017)","journal-title":"Found. Trends Programm. Lang."},{"issue":"1","key":"8_CR42","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s10009-010-0146-x","volume":"13","author":"EM Hahn","year":"2011","unstructured":"Hahn, E.M., Hermanns, H., Zhang, L.: Probabilistic reachability for parametric markov models. Softw. Tools Technol. Transf. 13(1), 3\u201319 (2011)","journal-title":"Softw. Tools Technol. Transf."},{"issue":"4","key":"8_CR43","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/s00450-013-0251-7","volume":"28","author":"TA Henzinger","year":"2013","unstructured":"Henzinger, T.A.: Quantitative reactive modeling and verification. Comput. Sci.- Res. Dev. 28(4), 331\u2013344 (2013)","journal-title":"Comput. Sci.- Res. Dev."},{"key":"8_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/978-3-540-78917-8_3","volume-title":"Formal Methods and Testing","author":"A Hessel","year":"2008","unstructured":"Hessel, A., Larsen, K.G., Mikucionis, M., Nielsen, B., Pettersson, P., Skou, A.: Testing real-time systems using UPPAAL. In: Hierons, R.M., Bowen, J.P., Harman, M. (eds.) Formal Methods and Testing. LNCS, vol. 4949, pp. 77\u2013117. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78917-8_3"},{"key":"8_CR45","doi-asserted-by":"crossref","unstructured":"Jansen, N., Humphrey, L.R., Tumova, J., Topcu, U.: Structured synthesis for probabilistic systems. CoRR abs\/1807.06106, at NFM 2019 (2018, to appear)","DOI":"10.1007\/978-3-030-20652-9_16"},{"key":"8_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"130","DOI":"10.1007\/978-3-662-49674-9_8","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Junges","year":"2016","unstructured":"Junges, S., Jansen, N., Dehnert, C., Topcu, U., Katoen, J.-P.: Safety-constrained reinforcement learning for MDPs. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 130\u2013146. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49674-9_8"},{"key":"8_CR47","unstructured":"Junges, S., et al.: Finite-state controllers of POMDPs using parameter synthesis. In: UAI, pp. 519\u2013529. AUAI Press (2018)"},{"issue":"1\u20132","key":"8_CR48","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1016\/S0004-3702(98)00023-X","volume":"101","author":"LP Kaelbling","year":"1998","unstructured":"Kaelbling, L.P., Littman, M.L., Cassandra, A.R.: Planning and acting in partially observable stochastic domains. Artif. Intell. 101(1\u20132), 99\u2013134 (1998)","journal-title":"Artif. Intell."},{"key":"8_CR49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/978-3-319-63121-9_3","volume-title":"Models, Algorithms, Logics and Tools","author":"J K\u0159et\u00ednsk\u00fd","year":"2017","unstructured":"K\u0159et\u00ednsk\u00fd, J.: 30 years of modal transition systems: survey of extensions and analysis. In: Aceto, L., Bacci, G., Bacci, G., Ing\u00f3lfsd\u00f3ttir, A., Legay, A., Mardare, R. (eds.) Models, Algorithms, Logics and Tools. LNCS, vol. 10460, pp. 36\u201374. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63121-9_3"},{"key":"8_CR50","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). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_47"},{"issue":"12\u201313","key":"8_CR51","doi-asserted-by":"publisher","first-page":"1272","DOI":"10.1016\/j.tcs.2008.12.058","volume":"410","author":"MZ Kwiatkowska","year":"2009","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D., Vigliotti, M.G.: Probabilistic mobile ambients. Theor. Comput. Sci. 410(12\u201313), 1272\u20131303 (2009)","journal-title":"Theor. Comput. Sci."},{"key":"8_CR52","unstructured":"Larsen, K.G.: Verification and performance analysis of embedded and cyber-physical systems using UPPAAL. In: MODELSWARD 2014, pp. IS-11 (2014)"},{"key":"8_CR53","unstructured":"Larsen, K.G., Thomsen, B.: A modal process logic. In: LICS, pp. 203\u2013210. IEEE Computer Society (1988)"},{"issue":"2","key":"8_CR54","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1145\/288197.581195","volume":"26","author":"C Lindemann","year":"1998","unstructured":"Lindemann, C.: Performance modelling with deterministic and stochastic Petri nets. Perf. Eval. Review 26(2), 3 (1998)","journal-title":"Perf. Eval. Review"},{"key":"8_CR55","unstructured":"Meuleau, N., Kim, K.E., Kaelbling, L.P., Cassandra, A.R.: Solving POMDPs by searching the space of finite policies. In: UAI, pp. 417\u2013426. Morgan Kaufmann Publishers Inc. (1999)"},{"key":"8_CR56","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., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"8_CR57","doi-asserted-by":"crossref","unstructured":"Nori, A.V., Ozair, S., Rajamani, S.K., Vijaykeerthy, D.: Efficient synthesis of probabilistic programs. In: PLDI, pp. 208\u2013217. ACM (2015)","DOI":"10.1145\/2813885.2737982"},{"key":"8_CR58","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/978-3-319-46520-3_4","volume-title":"Automated Technology for Verification and Analysis","author":"T Quatmann","year":"2016","unstructured":"Quatmann, T., Dehnert, C., Jansen, N., Junges, S., Katoen, J.-P.: Parameter synthesis for Markov models: faster than ever. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 50\u201367. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-46520-3_4"},{"key":"8_CR59","doi-asserted-by":"crossref","unstructured":"Rodrigues, et al.: Modeling and verification for probabilistic properties in software product lines. In: HASE, pp. 173\u2013180. IEEE (2015)","DOI":"10.1109\/HASE.2015.34"},{"key":"8_CR60","doi-asserted-by":"crossref","unstructured":"Rosenblum, D.S.: The power of probabilistic thinking. In: ASE, p. 3. ACM (2016)","DOI":"10.1145\/2970276.2985780"},{"issue":"4","key":"8_CR61","doi-asserted-by":"publisher","first-page":"493","DOI":"10.1016\/j.jss.2006.07.021","volume":"80","author":"VS Sharma","year":"2007","unstructured":"Sharma, V.S., Trivedi, K.S.: Quantifying software performance, reliability and security: an architecture-based approach. J. Syst. Softw. 80(4), 493\u2013509 (2007)","journal-title":"J. Syst. Softw."},{"key":"8_CR62","doi-asserted-by":"crossref","unstructured":"Solar-Lezama, A., Jones, C.G., Bodik, R.: Sketching concurrent data structures. In: PLDI, pp. 136\u2013148. ACM (2008)","DOI":"10.1145\/1379022.1375599"},{"key":"8_CR63","doi-asserted-by":"crossref","unstructured":"Solar-Lezama, A., Rabbah, R.M., Bod\u00edk, R., Ebcioglu, K.: Programming by sketching for bit-streaming programs. In: PLDI, pp. 281\u2013294. ACM (2005)","DOI":"10.1145\/1064978.1065045"},{"key":"8_CR64","doi-asserted-by":"crossref","unstructured":"Solar-Lezama, A., Tancau, L., Bodik, R., Seshia, S., Saraswat, V.: Combinatorial sketching for finite programs. In: ASPLOS, pp. 404\u2013415. ACM (2006)","DOI":"10.1145\/1168919.1168907"},{"key":"8_CR65","doi-asserted-by":"crossref","unstructured":"Stewart, W.J.: Probability, Markov Chains, Queues, and Simulation: The Mathematical Basis of Performance Modeling. Princeton university press (2009)","DOI":"10.1515\/9781400832811"},{"key":"8_CR66","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1007\/978-3-319-95582-7_19","volume-title":"Formal Methods","author":"A Vandin","year":"2018","unstructured":"Vandin, A., ter Beek, M.H., Legay, A., Lluch Lafuente, A.: QFLan: a tool for the quantitative analysis of highly reconfigurable systems. In: Havelund, K., Peleska, J., Roscoe, B., de Vink, E. (eds.) FM 2018. LNCS, vol. 10951, pp. 329\u2013337. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-95582-7_19"},{"key":"8_CR67","doi-asserted-by":"crossref","unstructured":"Varshosaz, M., Khosravi, R.: Discrete time Markov chain families: modeling and verification of probabilistic software product lines. In: SPLC Workshops, pp. 34\u201341. ACM (2013)","DOI":"10.1145\/2499777.2500725"},{"key":"8_CR68","doi-asserted-by":"crossref","unstructured":"\u010ce\u0161ka, M., Hensel, C., Junges, S., Katoen, J.P.: Counterexample-driven synthesis for probabilistic program sketches. CoRR abs\/1904.12371 (2019)","DOI":"10.1007\/978-3-030-30942-8_8"},{"issue":"4","key":"8_CR69","doi-asserted-by":"publisher","first-page":"12:1","DOI":"10.1145\/2382559.2382563","volume":"4","author":"N Vlassis","year":"2012","unstructured":"Vlassis, N., Littman, M.L., Barber, D.: On the computational complexity of stochastic controller optimization in POMDPs. ACM Trans. Comput. Theor. 4(4), 12:1\u201312:8 (2012). https:\/\/doi.org\/10.1145\/2382559.2382563","journal-title":"ACM Trans. Comput. Theor."},{"key":"8_CR70","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/978-3-642-28756-5_21","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Wimmer","year":"2012","unstructured":"Wimmer, R., Jansen, N., \u00c1brah\u00e1m, E., Becker, B., Katoen, J.-P.: Minimal critical subsystems for discrete-time Markov models. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 299\u2013314. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28756-5_21"},{"key":"8_CR71","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/978-3-642-40196-1_4","volume-title":"QEST 2013","author":"R Wimmer","year":"2013","unstructured":"Wimmer, R., Jansen, N., Vorpahl, A., \u00c1brah\u00e1m, E., Katoen, J.-P., Becker, B.: High-Level Counterexamples for Probabilistic Automata. In: Joshi, K., Siegle, M., Stoelinga, M., D\u2019Argenio, P.R. (eds.) QEST 2013. LNCS, vol. 8054, pp. 39\u201354. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40196-1_4"},{"issue":"4","key":"8_CR72","doi-asserted-by":"publisher","first-page":"1529","DOI":"10.1007\/s10270-013-0385-x","volume":"13","author":"M Woodside","year":"2014","unstructured":"Woodside, M., Petriu, D., Merseguer, J., Petriu, D., Alhaj, M.: Transformation challenges: from software models to performance models. J. Softw. Syst. Model. 13(4), 1529\u20131552 (2014)","journal-title":"J. Softw. Syst. Model."},{"issue":"1\u20132","key":"8_CR73","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/S0304-3975(97)00056-X","volume":"176","author":"S Wu","year":"1997","unstructured":"Wu, S., Smolka, S.A., Stark, E.W.: Composition and behaviors of probabilistic I\/O automata. Theor. Comput. Sci. 176(1\u20132), 1\u201338 (1997)","journal-title":"Theor. Comput. Sci."},{"key":"8_CR74","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"662","DOI":"10.1007\/978-3-319-96145-3_38","volume-title":"Computer Aided Verification","author":"W Zhou","year":"2018","unstructured":"Zhou, W., Li, W.: Safety-aware apprenticeship learning. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 662\u2013680. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_38"}],"container-title":["Lecture Notes in Computer Science","Formal Methods \u2013 The Next 30 Years"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-30942-8_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,29]],"date-time":"2022-09-29T07:17:20Z","timestamp":1664435840000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-30942-8_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030309411","9783030309428"],"references-count":74,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-30942-8_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"23 September 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Porto","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 October 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 October 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/formalmethods2019.inesctec.pt\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"129","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":"44","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":"7","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":"34% - 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":"5,5","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":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}