{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T14:51:54Z","timestamp":1742914314013,"version":"3.40.3"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031757822"},{"type":"electronic","value":"9783031757839"}],"license":[{"start":{"date-parts":[[2024,11,13]],"date-time":"2024-11-13T00:00:00Z","timestamp":1731456000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,11,13]],"date-time":"2024-11-13T00:00:00Z","timestamp":1731456000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-3-031-75783-9_13","type":"book-chapter","created":{"date-parts":[[2024,11,12]],"date-time":"2024-11-12T06:27:07Z","timestamp":1731392827000},"page":"322-338","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Towards a\u00a0Proof System for\u00a0Probabilistic Dynamic Logic"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5382-3949","authenticated-orcid":false,"given":"Einar Broch","family":"Johnsen","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0996-2543","authenticated-orcid":false,"given":"Eduard","family":"Kamburjan","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0003-7295","authenticated-orcid":false,"given":"Raul","family":"Pardo","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0007-9712-3224","authenticated-orcid":false,"given":"Erik","family":"Voogd","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0532-2685","authenticated-orcid":false,"given":"Andrzej","family":"W\u0105sowski","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,11,13]]},"reference":[{"key":"13_CR1","doi-asserted-by":"publisher","unstructured":"Ahrendt, W., Beckert, B., Bubel, R., H\u00e4hnle, R., Schmitt, P.H., Ulbrich, M. (eds.): Deductive Software Verification - The KeY Book - From Theory to Practice. LNCS, vol. 10001. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-319-49812-6","DOI":"10.1007\/978-3-319-49812-6"},{"key":"13_CR2","doi-asserted-by":"publisher","unstructured":"Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P.: Model-checking algorithms for continuous-time Markov chains. IEEE Trans. Software Eng. 29(6), 524\u2013541 (2003). https:\/\/doi.org\/10.1109\/TSE.2003.1205180","DOI":"10.1109\/TSE.2003.1205180"},{"key":"13_CR3","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"13_CR4","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.: Approximative symbolic model checking of continuous-time Markov chains. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664, pp. 146\u2013161. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48320-9_12"},{"key":"13_CR5","doi-asserted-by":"publisher","unstructured":"Batz, K., Biskup, T.J., Katoen, J.-P., Winkler, T.: Programmatic strategy synthesis: resolving nondeterminism in probabilistic programs. Proc. ACM Program. Lang. 8(POPL), 2792\u20132820 (2024). https:\/\/doi.org\/10.1145\/3632935","DOI":"10.1145\/3632935"},{"key":"13_CR6","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"410","DOI":"10.1007\/978-3-031-30820-8_25","volume-title":"TACAS 2023","author":"K Batz","year":"2023","unstructured":"Batz, K., Chen, M., Junges, S., Kaminski, B.L., Katoen, J.-P., Matheja, C.: Probabilistic program verification via inductive synthesis of inductive invariants. In: Sankaranarayanan, S., Sharygina, N. (eds.) TACAS 2023. LNCS, vol. 13994, pp. 410\u2013429. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-30820-8_25"},{"key":"13_CR7","doi-asserted-by":"publisher","unstructured":"Batz, K., Kaminski, B.L., Katoen, J.-P., Matheja, C.: Relatively complete verification of probabilistic programs: an expressive language for expectation-based reasoning. Proc. ACM Program. Lang. 5(POPL), 1\u201330 (2021). https:\/\/doi.org\/10.1145\/3434320","DOI":"10.1145\/3434320"},{"key":"13_CR8","doi-asserted-by":"publisher","unstructured":"Beckert, B., Klebanov, V., Wei\u00df, B.: Dynamic logic for Java. In: Ahrendt et\u00a0al. [1], pp. 49\u2013106. https:\/\/doi.org\/10.1007\/978-3-319-49812-6_3","DOI":"10.1007\/978-3-319-49812-6_3"},{"key":"13_CR9","doi-asserted-by":"publisher","unstructured":"de\u00a0Boer, F.S., Bonsangue, M.: Symbolic execution formally explained. Formal Aspects Comput. 33(4), 617\u2013636 (2021). https:\/\/doi.org\/10.1007\/s00165-020-00527-y","DOI":"10.1007\/s00165-020-00527-y"},{"key":"13_CR10","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":"13_CR11","doi-asserted-by":"publisher","unstructured":"Feng, S., Chen, M., Su, H., Kaminski, B.L., Katoen, J.-P., Zhan, N.: Lower bounds for possibly divergent probabilistic programs. Proc. ACM Program. Lang. 7(OOPSLA1), 696\u2013726 (2023). https:\/\/doi.org\/10.1145\/3586051","DOI":"10.1145\/3586051"},{"key":"13_CR12","doi-asserted-by":"publisher","unstructured":"H\u00e4hnle, R.: Dijkstra\u2019s legacy on program verification. In: Apt, K.R., Hoare, T. (eds.) Edsger Wybe Dijkstra: His Life, Work, and Legacy, pp. 105\u2013140. ACM\/Morgan & Claypool (2022). https:\/\/doi.org\/10.1145\/3544585.3544593","DOI":"10.1145\/3544585.3544593"},{"key":"13_CR13","doi-asserted-by":"crossref","unstructured":"Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. Foundations of Computing. MIT Press (2000)","DOI":"10.7551\/mitpress\/2516.001.0001"},{"key":"13_CR14","doi-asserted-by":"publisher","unstructured":"Hensel, C., Junges, S., Katoen, J.-P., Quatmann, T., Volk, M.: The probabilistic model checker Storm. Int. J. Softw. Tools Technol. Transf. 24(4), 589\u2013610 (2022). https:\/\/doi.org\/10.1007\/s10009-021-00633-z","DOI":"10.1007\/s10009-021-00633-z"},{"key":"13_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/978-3-642-25271-6_8","volume-title":"Formal Methods for Components and Objects","author":"EB Johnsen","year":"2011","unstructured":"Johnsen, E.B., H\u00e4hnle, R., Sch\u00e4fer, J., Schlatte, R., Steffen, M.: ABS: a core language for abstract behavioral specification. In: Aichernig, B.K., de Boer, F.S., Bonsangue, M.M. (eds.) FMCO 2010. LNCS, vol. 6957, pp. 142\u2013164. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-25271-6_8"},{"key":"13_CR16","doi-asserted-by":"publisher","unstructured":"Junges, S., et al.: Parameter synthesis for Markov models: covering the parameter space. Formal Methods Syst. Des. 62(1), 181\u2013259 (2024). https:\/\/doi.org\/10.1007\/s10703-023-00442-x","DOI":"10.1007\/s10703-023-00442-x"},{"key":"13_CR17","doi-asserted-by":"publisher","unstructured":"Kamburjan, E., Scaletta, M., Rollshausen, N.: Deductive verification of active objects with Crowbar. Sci. Comput. Program. 226, 102928 (2023). https:\/\/doi.org\/10.1016\/j.scico.2023.102928","DOI":"10.1016\/j.scico.2023.102928"},{"key":"13_CR18","unstructured":"Kaminski, B.L.: Advanced weakest precondition calculi for probabilistic programs. Ph.D. thesis, RWTH Aachen University, Germany (2019). http:\/\/publications.rwth-aachen.de\/record\/755408"},{"key":"13_CR19","doi-asserted-by":"publisher","unstructured":"Kaminski, B.L., Katoen, J.-P., Matheja, C., Olmedo, F.: Weakest precondition reasoning for expected runtimes of randomized algorithms. J. ACM 65(5), 30:1\u201330:68 (2018). https:\/\/doi.org\/10.1145\/3208102","DOI":"10.1145\/3208102"},{"key":"13_CR20","doi-asserted-by":"publisher","unstructured":"Kozen, D.: Semantics of probabilistic programs. In: Proceedings of 20th Annual Symposium on Foundations of Computer Science, pp. 101\u2013114. IEEE Computer Society (1979). https:\/\/doi.org\/10.1109\/SFCS.1979.38","DOI":"10.1109\/SFCS.1979.38"},{"key":"13_CR21","doi-asserted-by":"publisher","unstructured":"McIver, A., Morgan, C.: Abstraction, Refinement and Proof for Probabilistic Systems. Monographs in Computer Science. Springer, New York (2005). https:\/\/doi.org\/10.1007\/b138392","DOI":"10.1007\/b138392"},{"key":"13_CR22","doi-asserted-by":"publisher","unstructured":"McIver, A., Morgan, C., Kaminski, B.L., Katoen, J.-P.: A new proof rule for almost-sure termination. Proc. ACM Program. Lang. 2(POPL), 33:1\u201333:28 (2018). https:\/\/doi.org\/10.1145\/3158121","DOI":"10.1145\/3158121"},{"key":"13_CR23","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":"13_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-3-662-49122-5_2","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"P M\u00fcller","year":"2016","unstructured":"M\u00fcller, P., Schwerhoff, M., Summers, A.J.: Viper: a verification infrastructure for permission-based reasoning. In: Jobstmann, B., Leino, K.R.M. (eds.) VMCAI 2016. LNCS, vol. 9583, pp. 41\u201362. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49122-5_2"},{"key":"13_CR25","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1007\/978-3-031-17715-6_24","volume-title":"ICTAC 2022","author":"R Pardo","year":"2022","unstructured":"Pardo, R., Johnsen, E.B., Schaefer, I., W\u0105sowski, A.: A specification logic for programs in the probabilistic guarded command language. In: Seidl, H., Liu, Z., Pasareanu, C.S. (eds.) ICTAC 2022. LNCS, vol. 13572, pp. 369\u2013387. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-17715-6_24"},{"key":"13_CR26","unstructured":"Puterman, M.L.: Markov Decision Processes. Wiley, Hoboken (2005)"},{"key":"13_CR27","doi-asserted-by":"publisher","unstructured":"Schlatte, R., Johnsen, E.B., Kamburjan, E., Tapia\u00a0Tarifa, S.L.: The ABS simulator toolchain. Sci. Comput. Program. 223, 102861 (2022). https:\/\/doi.org\/10.1016\/j.scico.2022.102861","DOI":"10.1016\/j.scico.2022.102861"},{"key":"13_CR28","doi-asserted-by":"publisher","unstructured":"Schr\u00f6er, P., Batz, K., Kaminski, B.L., Katoen, J.-P., Matheja, C.: A deductive verification infrastructure for probabilistic programs. Proc. ACM Program. Lang. 7(OOPSLA2), 2052\u20132082 (2023). https:\/\/doi.org\/10.1145\/3622870","DOI":"10.1145\/3622870"},{"key":"13_CR29","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1007\/978-3-031-43835-6_23","volume-title":"QEST 2023","author":"E Voogd","year":"2023","unstructured":"Voogd, E., Johnsen, E.B., Silva, A., Susag, Z.J., W\u0105sowski, A.: Symbolic semantics for probabilistic programs. In: Jansen, N., Tribastone, M. (eds.) QEST 2023. LNCS, vol. 14287, pp. 329\u2013345. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-43835-6_23"}],"container-title":["Lecture Notes in Computer Science","Principles of Verification: Cycling the Probabilistic Landscape"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-75783-9_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,12]],"date-time":"2024-11-12T07:04:27Z","timestamp":1731395067000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-75783-9_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,11,13]]},"ISBN":["9783031757822","9783031757839"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-75783-9_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024,11,13]]},"assertion":[{"value":"13 November 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}