{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,29]],"date-time":"2025-11-29T07:51:12Z","timestamp":1764402672325},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319235059"},{"type":"electronic","value":"9783319235066"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-23506-6_4","type":"book-chapter","created":{"date-parts":[[2015,9,3]],"date-time":"2015-09-03T11:50:40Z","timestamp":1441281040000},"page":"15-32","source":"Crossref","is-referenced-by-count":15,"title":["Understanding Probabilistic Programs"],"prefix":"10.1007","author":[{"given":"Joost-Pieter","family":"Katoen","sequence":"first","affiliation":[]},{"given":"Friedrich","family":"Gretz","sequence":"additional","affiliation":[]},{"given":"Nils","family":"Jansen","sequence":"additional","affiliation":[]},{"given":"Benjamin Lucien","family":"Kaminski","sequence":"additional","affiliation":[]},{"given":"Federico","family":"Olmedo","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,11,10]]},"reference":[{"issue":"3","key":"4_CR1","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1145\/2492061","volume":"35","author":"G Barthe","year":"2013","unstructured":"Barthe, G., Kopf, B., Olmedo, F., B\u00e9guelin, S.Z.: Probabilistic relational reasoning for differential privacy. ACM Trans. Program. Lang. Syst. 35(3), 9 (2013)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"4_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1007\/978-3-319-10936-7_6","volume-title":"SAS 2014","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.) Static Analysis. LNCS, vol. 8723, pp. 85\u2013100. Springer, Heidelberg (2014)"},{"key":"4_CR3","doi-asserted-by":"publisher","first-page":"167","DOI":"10.4204\/EPTCS.102.15","volume":"102","author":"D Cock","year":"2012","unstructured":"Cock, D.: Verifying probabilistic correctness in Isabelle with pGCL. El. Proc. in Th. Comp. Sc. 102, 167\u2013178 (2012)","journal-title":"El. Proc. in Th. Comp. Sc."},{"key":"4_CR4","unstructured":"Dijkstra, E.W.: A Discipline of Programming. Prentice Hall (1976)"},{"key":"4_CR5","doi-asserted-by":"crossref","unstructured":"Feldman, Y.A., Harel, D.: A probabilistic dynamic logic. In: Proc. of STOC, pp. 181\u2013195. ACM (1982)","DOI":"10.1145\/800070.802191"},{"key":"4_CR6","unstructured":"Gordon, A.D.: An agenda for probabilistic programming: Usable, portable, and ubiquitous (2013). http:\/\/research.microsoft.com\/en-us\/projects\/fun"},{"key":"4_CR7","doi-asserted-by":"crossref","unstructured":"Gordon, A.D., Graepel, T., Rolland, N., Russo, C.V., Borgstr\u00f6m, J., Guiver, J.: Tabular: a schema-driven probabilistic programming language. In: Proc. of POPL, pp. 321\u2013334. ACM Press (2014)","DOI":"10.1145\/2535838.2535850"},{"key":"4_CR8","doi-asserted-by":"crossref","unstructured":"Gordon, A.D., Henzinger, T.A., Nori, A.V., Rajamani, S.K.: Probabilistic programming. In: Proc. of FOSE, pp. 167\u2013181. ACM Press (2014)","DOI":"10.1145\/2593882.2593900"},{"key":"4_CR9","doi-asserted-by":"crossref","unstructured":"Gretz, F., Jansen, N., Kaminski, B.L., Katoen, J.P., McIver, A., Olmedo, F.: Conditioning in probabilistic programming. In: Proc. of MFPS, p. 12 (2015)","DOI":"10.1016\/j.entcs.2015.12.013"},{"key":"4_CR10","doi-asserted-by":"crossref","unstructured":"Gretz, F., Jansen, N., Kaminski, B.L., Katoen, J.P., McIver, A., Olmedo, F.: Conditioning in probabilistic programming. CoRR (2015)","DOI":"10.1016\/j.entcs.2015.12.013"},{"key":"4_CR11","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."},{"key":"4_CR12","doi-asserted-by":"crossref","unstructured":"Hur, C.K., Nori, A.V., Rajamani, S.K., Samuel, S.: Slicing probabilistic programs. In: Proc. of PLDI, pp. 133\u2013144. ACM Press (2014)","DOI":"10.1145\/2666356.2594303"},{"issue":"1","key":"4_CR13","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":"4_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/978-3-662-48057-1_24","volume-title":"Mathematical Foundations of Computer Science 2015","author":"BL Kaminski","year":"2015","unstructured":"Kaminski, B.L., Katoen, J.-P.: On the hardness of almost\u2013sure termination. In: Italiano, G.F., Pighizzini, G., Sannella, D.T. (eds.) MFCS 2015. LNCS, vol. 9234, pp. 307\u2013318. Springer, Heidelberg (2015)"},{"key":"4_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"390","DOI":"10.1007\/978-3-642-15769-1_24","volume-title":"Static Analysis","author":"J-P Katoen","year":"2010","unstructured":"Katoen, J.-P., McIver, A.K., Meinicke, L.A., Morgan, C.C.: Linear-invariant generation for probabilistic programs. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 390\u2013406. Springer, Heidelberg (2010)"},{"issue":"3","key":"4_CR16","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(3), 328\u2013350 (1981)","journal-title":"J. Comput. Syst. Sci."},{"key":"4_CR17","unstructured":"McIver, A., Morgan, C.: Abstraction, Refinement and Proof for Probabilistic Systems. Springer (2004)"},{"key":"4_CR18","doi-asserted-by":"crossref","unstructured":"Motwani, R., Raghavan, P.: Randomized Algorithms. Cambridge University Press (1995)","DOI":"10.1017\/CBO9780511814075"},{"key":"4_CR19","doi-asserted-by":"crossref","unstructured":"Nori, A.V., Hur, C.K., Rajamani, S.K., Samuel, S.: R2: An efficient MCMC sampler for probabilistic programs. In: Proc. of AAAI. AAAI Press (July 2014)","DOI":"10.1609\/aaai.v28i1.9060"},{"key":"4_CR20","doi-asserted-by":"crossref","unstructured":"Olderog, E.R.: Nets, Terms and Formulas: Three Views of Concurrent Processes and their Relationship. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press (1990)","DOI":"10.1017\/CBO9780511526589"},{"key":"4_CR21","unstructured":"Paige, B., Wood, F.: A compilation target for probabilistic programming languages. In: Proc. of ICML. JMLR Proceedings, vol. 32, pp. 1935\u20131943. JMLR.org. (2014)"},{"key":"4_CR22","unstructured":"Pfeffer, A.: Figaro: An object-oriented probabilistic programming language. Technical report, Charles River Analytics (2000)"},{"key":"4_CR23","doi-asserted-by":"crossref","unstructured":"Puterman, M.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. John Wiley and Sons (1994)","DOI":"10.1002\/9780470316887"},{"key":"4_CR24","doi-asserted-by":"crossref","unstructured":"Sampson, A., Panchekha, P., Mytkowicz, T., McKinley, K.S., Grossman, D., Ceze, L.: Expressing and verifying probabilistic assertions. In: Proc. of PLDI, p. 14. ACM (2014)","DOI":"10.1145\/2594291.2594294"},{"issue":"2","key":"4_CR25","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 Journal on Computing 13(2), 292\u2013314 (1984)","journal-title":"SIAM Journal on Computing"},{"key":"4_CR26","doi-asserted-by":"crossref","unstructured":"Shoup, V.: A Computational Introduction to Number Theory and Algebra. Cambridge University Press (2009)","DOI":"10.1017\/CBO9780511814549"}],"container-title":["Lecture Notes in Computer Science","Correct System Design"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-23506-6_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,13]],"date-time":"2023-08-13T18:13:09Z","timestamp":1691950389000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-23506-6_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319235059","9783319235066"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-23506-6_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}