{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:34:28Z","timestamp":1767929668439,"version":"3.49.0"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783031177149","type":"print"},{"value":"9783031177156","type":"electronic"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"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":[[2022]]},"DOI":"10.1007\/978-3-031-17715-6_24","type":"book-chapter","created":{"date-parts":[[2022,10,2]],"date-time":"2022-10-02T09:02:27Z","timestamp":1664701347000},"page":"369-387","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["A Specification Logic for\u00a0Programs in\u00a0the\u00a0Probabilistic Guarded Command Language"],"prefix":"10.1007","author":[{"given":"Ra\u00fal","family":"Pardo","sequence":"first","affiliation":[]},{"given":"Einar Broch","family":"Johnsen","sequence":"additional","affiliation":[]},{"given":"Ina","family":"Schaefer","sequence":"additional","affiliation":[]},{"given":"Andrzej","family":"W\u0105sowski","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,10,3]]},"reference":[{"key":"24_CR1","doi-asserted-by":"crossref","unstructured":"Kozen, D.: Semantics of probabilistic programs. In: Proceedings 20th Annual Symposium on Foundations of Computer Science, IEEE Computer Society, 101\u2013114 (1979)","DOI":"10.1109\/SFCS.1979.38"},{"key":"24_CR2","doi-asserted-by":"crossref","unstructured":"Hark, M., Kaminski, B.L., Giesl, J., Katoen, J.: Aiming low is harder: induction for lower bounds in probabilistic program verification. In: Proceedings of ACM Programming Language, 4(POPL), pp. 37:1\u201337:28 (2020)","DOI":"10.1145\/3371105"},{"key":"24_CR3","unstructured":"Kaminski, B.L.: Advanced weakest precondition calculi for probabilistic programs. PhD thesis, RWTH Aachen University, Germany (2019)"},{"key":"24_CR4","doi-asserted-by":"crossref","unstructured":"Stein, D., Staton, S.: Compositional semantics for probabilistic programs with exact conditioning. In: Proceedings on 36th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS 2021), pp. 1\u201313 IEEE (2021)","DOI":"10.1109\/LICS52264.2021.9470552"},{"key":"24_CR5","doi-asserted-by":"crossref","unstructured":"Smolka, S., Kumar, P., Foster, N., Kozen, D., Silva, A.: Cantor meets Scott: semantic foundations for probabilistic networks. In: Castagna, G., Gordon, A.D., (eds.) Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2017), pp. 557\u2013571. ACM (2017)","DOI":"10.1145\/3009837.3009843"},{"key":"24_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/978-3-030-99336-8_3","volume-title":"Programming Languages and Systems","author":"K Batz","year":"2022","unstructured":"Batz, K., et al.: Foundations for entailment checking in quantitative separation logic. In: Sergey, I. (ed.) ESOP 2022. LNCS, vol. 13240, pp. 57\u201384. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99336-8_3"},{"key":"24_CR7","doi-asserted-by":"crossref","unstructured":"McIver, A., Morgan, C.: Abstraction, Refinement And Proof For Probabilistic Systems. Monographs in Computer Science. Springer, Cham (2005)","DOI":"10.1145\/1059816.1059824"},{"key":"24_CR8","unstructured":"Dijkstra, E.W.: A discipline of programming. Prentice-Hall (1976)"},{"key":"24_CR9","series-title":"Foundations of Computing","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/2516.001.0001","volume-title":"Dynamic Logic","author":"D Harel","year":"2000","unstructured":"Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. Foundations of Computing, MIT Press, Cambridge (2000)"},{"issue":"5","key":"24_CR10","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/BF01211866","volume":"6","author":"H Hansson","year":"1994","unstructured":"Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects Comput. 6(5), 512\u2013535 (1994)","journal-title":"Formal Aspects Comput."},{"key":"24_CR11","volume-title":"Markov Decision Processes","author":"ML Puterman","year":"2005","unstructured":"Puterman, M.L.: Markov Decision Processes. Wiley, Hoboken (2005)"},{"key":"24_CR12","series-title":"Lecture Notes in Computer Science","volume-title":"Deductive Software Verification - The KeY Book - From Theory to Practice","year":"2016","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. Lecture Notes in Computer Science, vol. 10001. Springer, Cham (2016)"},{"key":"24_CR13","doi-asserted-by":"crossref","unstructured":"de Gouw, S., Rot, J., de Boer, F.S., Bubel, R., H\u00e4hnle, R.: OpenJDK\u2019s Java.utils.Collection.sort() is broken: The good, the bad and the worst case. In: Kroening, D., Pasareanu, C.S., (eds.) Proceedings of 27th International Conference on Computer Aided Verification (CAV 2015), Lecture Notes in Computer Science, vol. 9206, pp. 273\u2013289 Springer, Cham (2015)","DOI":"10.1007\/978-3-319-21690-4_16"},{"key":"24_CR14","doi-asserted-by":"crossref","unstructured":"Pardo, R., Johnsen, E.B., Schaefer, I., W\u0105sowski, A.: A specification logic for programs in the probabilistic guarded command language (extended version). ArXiv: https:\/\/arxiv.org\/abs\/2205.04822 (2022)","DOI":"10.1007\/978-3-031-17715-6_24"},{"key":"24_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/978-3-642-28869-2_9","volume-title":"Programming Languages and Systems","author":"P Cousot","year":"2012","unstructured":"Cousot, P., Monerau, M.: Probabilistic abstract interpretation. In: Seidl, H. (ed.) ESOP 2012. LNCS, vol. 7211, pp. 169\u2013193. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28869-2_9"},{"key":"24_CR16","doi-asserted-by":"crossref","unstructured":"Filieri, A., Pasareanu, C.S., Visser, W.: Reliability analysis in symbolic pathfinder. In: 35th International Conference on Software Engineering (ICSE 2013). IEEE Computer Society, pp. 622\u2013631 (2013)","DOI":"10.1109\/ICSE.2013.6606608"},{"key":"24_CR17","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D.: The PRISM benchmark suite. In: Ninth International Conference on Quantitative Evaluation of Systems (QEST 2012). IEEE Computer Society, pp. 203\u2013204 (2012)","DOI":"10.1109\/QEST.2012.14"},{"issue":"2","key":"24_CR18","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1016\/0022-0000(85)90012-1","volume":"30","author":"D Kozen","year":"1985","unstructured":"Kozen, D.: A probabilistic PDL. J. Comput. Syst. Sci. 30(2), 162\u2013178 (1985)","journal-title":"J. Comput. Syst. Sci."},{"key":"24_CR19","doi-asserted-by":"crossref","unstructured":"Feldman, Y.A., Harel, D.: A probabilistic dynamic logic. In: Proceedings of the 14th Annual ACM Symposium on Theory of Computing (STOC), pp. 181\u2013195. ACM (1982)","DOI":"10.1145\/800070.802191"},{"issue":"POPL","key":"24_CR20","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3434320","volume":"5","author":"K Batz","year":"2021","unstructured":"Batz, K., Kaminski, B.L., Katoen, J., Matheja, C.: Relatively complete verification of probabilistic programs: an expressive language for expectation-based reasoning. Proc. ACM Program. Lang. 5(POPL), 1\u201330 (2021)","journal-title":"Proc. ACM Program. Lang."},{"key":"24_CR21","doi-asserted-by":"crossref","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. ACM \/ Morgan & Claypool, pp. 105\u2013140 (2022)","DOI":"10.1145\/3544585.3544593"},{"key":"24_CR22","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1016\/j.peva.2013.11.004","volume":"73","author":"F Gretz","year":"2014","unstructured":"Gretz, F., Katoen, J., McIver, A.: Operational versus weakest pre-expectation semantics for the probabilistic guarded command language. Perform. Eval. 73, 110\u2013132 (2014)","journal-title":"Perform. Eval."},{"key":"24_CR23","doi-asserted-by":"crossref","unstructured":"McIver, A., Morgan, C., Kaminski, B.L., Katoen, J.: A new proof rule for almost-sure termination. Proc. ACM Program. Lang. 2(POPL), 33:1\u201333:28 (2018)","DOI":"10.1145\/3158121"},{"key":"24_CR24","doi-asserted-by":"crossref","unstructured":"Batz, K., Kaminski, B.L., Katoen, J., Matheja, C., Noll, T.: Quantitative separation logic: a logic for reasoning about probabilistic pointer programs. Proc. ACM Program. Lang. 3(POPL), 34:1\u201334:29 (2019)","DOI":"10.1145\/3290347"},{"key":"24_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/978-3-662-49498-1_15","volume-title":"Programming Languages and Systems","author":"BL Kaminski","year":"2016","unstructured":"Kaminski, B.L., Katoen, J.-P., Matheja, C., Olmedo, F.: Weakest precondition reasoning for expected run\u2013times of probabilistic programs. In: Thiemann, P. (ed.) ESOP 2016. LNCS, vol. 9632, pp. 364\u2013389. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49498-1_15"},{"key":"24_CR26","doi-asserted-by":"crossref","unstructured":"Aguirre, A., Barthe, G., Hsu, J., Kaminski, B.L., Katoen, J., Matheja, C.: A pre-expectation calculus for probabilistic sensitivity. Proc. ACM Program. Lang. 5(POPL), 1\u201328 (2021)","DOI":"10.1145\/3434333"},{"key":"24_CR27","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1016\/S1571-0661(05)80595-X","volume":"22","author":"C Baier","year":"1999","unstructured":"Baier, C., Kwiatkowska, M.Z., Norman, G.: Computing probability bounds for linear time formulas over concurrent probabilistic systems. Electron. Notes Theor. Comput. Sci. 22, 29 (1999)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"24_CR28","series-title":"Springer Texts in Statistics","doi-asserted-by":"publisher","DOI":"10.1007\/1-84628-168-7","volume-title":"A Modern Introduction to Probability and Statistics: Understanding Why and How","author":"FM Dekking","year":"2005","unstructured":"Dekking, F.M., Kraaikamp, C., Lopuha\u00e4, H.P., Meester, L.E.: A Modern Introduction to Probability and Statistics: Understanding Why and How. STS, Springer, London (2005). https:\/\/doi.org\/10.1007\/1-84628-168-7"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing \u2013 ICTAC 2022"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-17715-6_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,10,2]],"date-time":"2022-10-02T23:05:04Z","timestamp":1664751904000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-17715-6_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031177149","9783031177156"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-17715-6_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"3 October 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ICTAC","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Colloquium on Theoretical Aspects of Computing","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Tbilisi","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Georgia","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 September 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 September 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ictac2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/viam.science.tsu.ge\/clas2022\/ictac\/index.html","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}