{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T03:10:06Z","timestamp":1775790606258,"version":"3.50.1"},"publisher-location":"Cham","reference-count":42,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319898834","type":"print"},{"value":"9783319898841","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-89884-1_5","type":"book-chapter","created":{"date-parts":[[2018,4,13]],"date-time":"2018-04-13T21:02:32Z","timestamp":1523653352000},"page":"117-144","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":20,"title":["An Assertion-Based Program Logic for Probabilistic Programs"],"prefix":"10.1007","author":[{"given":"Gilles","family":"Barthe","sequence":"first","affiliation":[]},{"given":"Thomas","family":"Espitau","sequence":"additional","affiliation":[]},{"given":"Marco","family":"Gaboardi","sequence":"additional","affiliation":[]},{"given":"Benjamin","family":"Gr\u00e9goire","sequence":"additional","affiliation":[]},{"given":"Justin","family":"Hsu","sequence":"additional","affiliation":[]},{"given":"Pierre-Yves","family":"Strub","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,4,14]]},"reference":[{"key":"5_CR1","doi-asserted-by":"publisher","unstructured":"Baier, C.: Probabilistic model checking. In: Dependable Software Systems Engineering, NATO Science for Peace and Security Series - D: Information and Communication Security, vol. 45, pp. 1\u201323. IOS Press (2016), https:\/\/doi.org\/10.3233\/978-1-61499-627-9-1","DOI":"10.3233\/978-1-61499-627-9-1"},{"key":"5_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/978-3-319-10082-1_6","volume-title":"Foundations of Security Analysis and Design VII","author":"G Barthe","year":"2014","unstructured":"Barthe, G., Dupressoir, F., Gr\u00e9goire, B., Kunz, C., Schmidt, B., Strub, P.-Y.: EasyCrypt: A tutorial. In: Aldini, A., Lopez, J., Martinelli, F. (eds.) FOSAD 2012-2013. LNCS, vol. 8604, pp. 146\u2013166. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-10082-1_6"},{"key":"5_CR3","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1007\/978-3-319-41528-4_3","volume-title":"Computer Aided Verification","author":"Gilles Barthe","year":"2016","unstructured":"Barthe, G., Espitau, T., Ferrer Fioriti, L.M., Hsu, J.: Synthesizing probabilistic invariants via Doob\u2019s decomposition. In: International Conference on Computer Aided Verification (CAV), Toronto, Ontario (2016). https:\/\/arxiv.org\/abs\/1605.02765"},{"key":"5_CR4","unstructured":"Barthe, G., Gaboardi, M., Gr\u00e9goire, B., Hsu, J., Strub, P.Y.: A program logic for union bounds. In: International Colloquium on Automata, Languages and Programming (ICALP), Rome, Italy (2016). http:\/\/arxiv.org\/abs\/1602.05681"},{"key":"5_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/978-3-642-22792-9_5","volume-title":"Advances in Cryptology \u2013 CRYPTO 2011","author":"G Barthe","year":"2011","unstructured":"Barthe, G., Gr\u00e9goire, B., Heraud, S., B\u00e9guelin, S.Z.: Computer-aided security proofs for the working cryptographer. In: Rogaway, P. (ed.) CRYPTO 2011. LNCS, vol. 6841, pp. 71\u201390. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22792-9_5"},{"key":"5_CR6","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1007\/11761679_25","volume-title":"Advances in Cryptology - EUROCRYPT 2006","author":"Mihir Bellare","year":"2006","unstructured":"Bellare, M., Rogaway, P.: The security of triple encryption and a framework for code-based game-playing proofs. In: IACR International Conference on the Theory and Applications of Cryptographic Techniques (EUROCRYPT), Saint Petersburg, Russia, pp. 409\u2013426 (2006). https:\/\/doi.org\/10.1007\/11761679_25"},{"key":"5_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/978-3-662-46678-0_18","volume-title":"Foundations of Software Science and Computation Structures","author":"A Bizjak","year":"2015","unstructured":"Bizjak, A., Birkedal, L.: Step-indexed logical relations for probability. In: Pitts, A. (ed.) FoSSaCS 2015. LNCS, vol. 9034, pp. 279\u2013294. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46678-0_18"},{"issue":"1\u20132","key":"5_CR8","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/j.tcs.2007.02.040","volume":"379","author":"R Chadha","year":"2007","unstructured":"Chadha, R., Cruz-Filipe, L., Mateus, P., Sernadas, A.: Reasoning about probabilistic sequential programs. Theoretical Computer Science 379(1\u20132), 142\u2013165 (2007)","journal-title":"Theoretical Computer Science"},{"key":"5_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1007\/978-3-642-39799-8_34","volume-title":"Computer Aided Verification","author":"A Chakarov","year":"2013","unstructured":"Chakarov, A., Sankaranarayanan, S.: Probabilistic program analysis with martingales. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 511\u2013526. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_34"},{"key":"5_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/978-3-319-10936-7_6","volume-title":"Static Analysis","author":"A Chakarov","year":"2014","unstructured":"Chakarov, A., Sankaranarayanan, S.: Expectation invariants for probabilistic program loops as fixed points. In: M\u00fcller-Olm, M., Seidl, H. (eds.) SAS 2014. LNCS, vol. 8723, pp. 85\u2013100. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-10936-7_6"},{"key":"5_CR11","doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Fu, H., Novotn\u00fd, P., Hasheminezhad, R.: Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs. In: ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), Saint Petersburg, Florida, pp. 327\u2013342 (2016). https:\/\/doi.org\/10.1145\/2837614.2837639","DOI":"10.1145\/2837614.2837639"},{"key":"5_CR12","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":"5_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/978-3-642-54833-8_12","volume-title":"Programming Languages and Systems","author":"R Crubill\u00e9","year":"2014","unstructured":"Crubill\u00e9, R., Dal Lago, U.: On probabilistic applicative bisimulation and call-by-value $$\\lambda $$\u03bb-calculi. In: Shao, Z. (ed.) ESOP 2014. LNCS, vol. 8410, pp. 209\u2013228. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54833-8_12"},{"key":"5_CR14","unstructured":"Dal Lago, U., Sangiorgi, D., Alberti, M.: On coinductive equivalences for higher-order probabilistic functional programs. In: ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), San Diego, California, pp. 297\u2013308 (2014). https:\/\/arxiv.org\/abs\/1311.1722"},{"key":"5_CR15","doi-asserted-by":"crossref","unstructured":"Fioriti, L.M.F., Hermanns, H.: Probabilistic termination: Soundness, completeness, and compositionality. In: ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), Mumbai, India, pp. 489\u2013501 (2015)","DOI":"10.1145\/2676726.2677001"},{"key":"5_CR16","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.P., McIver, A.: Operational versus weakest pre-expectation semantics for the probabilistic guarded command language. Perform. Eval. 73, 110\u2013132 (2014)","journal-title":"Perform. Eval."},{"issue":"3","key":"5_CR17","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1145\/2166.357214","volume":"5","author":"S Hart","year":"1983","unstructured":"Hart, S., Sharir, M., Pnueli, A.: Termination of probabilistic concurrent programs. ACM Trans. Program. Lang. Syst. 5(3), 356\u2013380 (1983)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"5_CR18","unstructured":"den Hartog, J.: Probabilistic extensions of semantical models. Ph.D. thesis, Vrije Universiteit Amsterdam (2002)"},{"key":"5_CR19","unstructured":"Hurd, J.: Formal verification of probabilistic algorithms. Technical report, UCAM-CL-TR-566, University of Cambridge, Computer Laboratory (2003)"},{"issue":"1\u20132","key":"5_CR20","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/S1567-8326(02)00065-6","volume":"56","author":"J Hurd","year":"2003","unstructured":"Hurd, J.: Verification of the Miller-Rabin probabilistic primality test. J. Log. Algebr. Program. 56(1\u20132), 3\u201321 (2003). https:\/\/doi.org\/10.1016\/S1567-8326(02)00065\u20136","journal-title":"J. Log. Algebr. Program."},{"issue":"1","key":"5_CR21","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1016\/j.tcs.2005.08.005","volume":"346","author":"J Hurd","year":"2005","unstructured":"Hurd, J., McIver, A., Morgan, C.: Probabilistic guarded commands mechanized in HOL. Theor. Comput. Sci. 346(1), 96\u2013112 (2005)","journal-title":"Theor. Comput. Sci."},{"key":"5_CR22","doi-asserted-by":"publisher","unstructured":"Impagliazzo, R., Rudich, S.: Limits on the provable consequences of one-way permutations. In: ACM SIGACT Symposium on Theory of Computing (STOC), Seattle, Washington, pp. 44\u201361 (1989). https:\/\/doi.org\/10.1145\/73007.73012","DOI":"10.1145\/73007.73012"},{"key":"5_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/978-3-319-43425-4_14","volume-title":"Quantitative Evaluation of Systems","author":"BL Kaminski","year":"2016","unstructured":"Kaminski, B.L., Katoen, J.-P., Matheja, C.: Inferring covariances for probabilistic programs. In: Agha, G., Van Houdt, B. (eds.) QEST 2016. LNCS, vol. 9826, pp. 191\u2013206. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-43425-4_14"},{"key":"5_CR24","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/978-3-662-49498-1_15","volume-title":"Programming Languages and Systems","author":"Benjamin Lucien Kaminski","year":"2016","unstructured":"Kaminski, B., Katoen, J.P., Matheja, C., Olmedo, F.: Weakest precondition reasoning for expected run-times of probabilistic programs. In: European Symposium on Programming (ESOP), Eindhoven, The Netherlands, January 2016"},{"key":"5_CR25","doi-asserted-by":"crossref","unstructured":"Katoen, J.P.: The probabilistic model-checking landscape. In: IEEE Symposium on Logic in Computer Science (LICS), New York (2016)","DOI":"10.1145\/2933575.2934574"},{"key":"5_CR26","doi-asserted-by":"publisher","unstructured":"Kempe, D., Dobra, A., Gehrke, J.: Gossip-based computation of aggregate information. In: Proceedings of the 44th Annual IEEE Symposium on Foundations of Computer Science, pp. 482\u2013491 (2003). https:\/\/doi.org\/10.1109\/SFCS.2003.1238221","DOI":"10.1109\/SFCS.2003.1238221"},{"key":"5_CR27","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1016\/0022-0000(81)90036-2","volume":"22","author":"D Kozen","year":"1981","unstructured":"Kozen, D.: Semantics of probabilistic programs. J. Comput. Syst. Sci. 22, 328\u2013350 (1981). https:\/\/www.sciencedirect.com\/science\/article\/pii\/0022000081900362","journal-title":"J. Comput. Syst. Sci."},{"issue":"2","key":"5_CR28","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":"5_CR29","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"},{"key":"5_CR30","series-title":"Monographs in Computer Science","volume-title":"Abstraction, refinement, and proof for probabilistic systems","author":"A McIver","year":"2005","unstructured":"McIver, A., Morgan, C.: Abstraction, refinement, and proof for probabilistic systems. Monographs in Computer Science. Springer, New York (2005)"},{"key":"5_CR31","doi-asserted-by":"crossref","unstructured":"McIver, A., Morgan, C., Kaminski, B.L., Katoen, J.P.: A new rule for almost-certain termination. In: Proceedings of the ACM on Programming Languages 1(POPL) (2018). https:\/\/arxiv.org\/abs\/1612.01091 , appeared at ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), Los Angeles, California","DOI":"10.1145\/3158121"},{"key":"5_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"322","DOI":"10.1007\/978-3-540-45099-3_17","volume-title":"Static Analysis","author":"D Monniaux","year":"2000","unstructured":"Monniaux, D.: Abstract interpretation of probabilistic semantics. In: Palsberg, J. (ed.) SAS 2000. LNCS, vol. 1824, pp. 322\u2013339. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/978-3-540-45099-3_17"},{"key":"5_CR33","doi-asserted-by":"crossref","unstructured":"Morgan, C.: Proof rules for probabilistic loops. In: BCS-FACS Conference on Refinement, Bath, England (1996)","DOI":"10.14236\/ewic\/RW1996.10"},{"issue":"3","key":"5_CR34","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1145\/229542.229547","volume":"18","author":"C Morgan","year":"1996","unstructured":"Morgan, C., McIver, A., Seidel, K.: Probabilistic predicate transformers. ACM Trans. Program. Lang. Syst. 18(3), 325\u2013353 (1996)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"5_CR35","doi-asserted-by":"crossref","unstructured":"Olmedo, F., Kaminski, B.L., Katoen, J.P., Matheja, C.: Reasoning about recursive probabilistic programs. In: IEEE Symposium on Logic in Computer Science (LICS), New York, pp. 672\u2013681 (2016)","DOI":"10.1145\/2933575.2935317"},{"key":"5_CR36","unstructured":"Pearl, J., Paz, A.: Graphoids: graph-based logic for reasoning about relevance relations. In: ECAI, pp. 357\u2013363 (1986)"},{"key":"5_CR37","unstructured":"Ramshaw, L.H.: Formalizing the Analysis of Algorithms. Ph.D. thesis, Computer Science (1979)"},{"key":"5_CR38","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1016\/j.entcs.2015.12.021","volume":"319","author":"Robert Rand","year":"2015","unstructured":"Rand, R., Zdancewic, S.: VPHL: a verified partial-correctness logic for probabilistic programs. In: Conference on the Mathematical Foundations of Programming Semantics (MFPS), Nijmegen, The Netherlands (2015)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"5_CR39","doi-asserted-by":"crossref","unstructured":"Sampson, A., Panchekha, P., Mytkowicz, T., McKinley, K.S., Grossman, D., Ceze, L.: Expressing and verifying probabilistic assertions. In: ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Edinburgh, Scotland, p. 14 (2014)","DOI":"10.1145\/2666356.2594294"},{"issue":"2","key":"5_CR40","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1137\/0213021","volume":"13","author":"M Sharir","year":"1984","unstructured":"Sharir, M., Pnueli, A., Hart, S.: Verification of probabilistic programs. SIAM J. Comput. 13(2), 292\u2013314 (1984)","journal-title":"SIAM J. Comput."},{"issue":"2","key":"5_CR41","doi-asserted-by":"publisher","first-page":"350","DOI":"10.1137\/0211027","volume":"11","author":"LG Valiant","year":"1982","unstructured":"Valiant, L.G.: A scheme for fast parallel communication. SIAM J. Comput. 11(2), 350\u2013361 (1982)","journal-title":"SIAM J. Comput."},{"key":"5_CR42","doi-asserted-by":"publisher","unstructured":"Valiant, L.G., Brebner, G.J.: Universal schemes for parallel communication. In: ACM SIGACT Symposium on Theory of Computing (STOC), Milwaukee, Wisconsin, pp. 263\u2013277 (1981). https:\/\/doi.org\/10.1145\/800076.802479","DOI":"10.1145\/800076.802479"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-89884-1_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,15]],"date-time":"2019-10-15T16:32:26Z","timestamp":1571157146000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-89884-1_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319898834","9783319898841"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-89884-1_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]}}}