{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T00:44:05Z","timestamp":1775868245845,"version":"3.50.1"},"reference-count":28,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2020,4,17]],"date-time":"2020-04-17T00:00:00Z","timestamp":1587081600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"US National Science Foundation","doi-asserted-by":"crossref","id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2020,6,30]]},"abstract":"<jats:p>Dedicated to the memory of Sebastian Danicic.<\/jats:p>\n          <jats:p>We present a theory for slicing imperative probabilistic programs containing random assignments and \u201cobserve\u201d statements for conditioning. We represent such programs as probabilistic control-flow graphs (pCFGs) whose nodes modify probability distributions. This allows direct adaptation of standard machinery such as data dependence, postdominators, relevant variables, and so on, to the probabilistic setting. We separate the specification of slicing from its implementation:<\/jats:p>\n          <jats:p>\n            (1) first, we develop syntactic conditions that a slice must satisfy (they involve the existence of another disjoint slice such that the variables of the two slices are\n            <jats:italic>probabilistically independent<\/jats:italic>\n            of each other);\n          <\/jats:p>\n          <jats:p>(2) next, we prove that any such slice is semantically correct;<\/jats:p>\n          <jats:p>(3) finally, we give an algorithm to compute the least slice.<\/jats:p>\n          <jats:p>To generate smaller slices, we may in addition take advantage of knowledge that certain loops will terminate (almost) always.<\/jats:p>\n          <jats:p>\n            Our results carry over to the slicing of\n            <jats:italic>structured<\/jats:italic>\n            imperative probabilistic programs, as handled in recent work by Hur et\u00a0al. For such a program, we can define its slice, which has the same \u201cnormalized\u201d semantics as the original program; the proof of this property is based on a result proving the adequacy of the semantics of pCFGs w.r.t.\u00a0the standard semantics of structured imperative probabilistic programs.\n          <\/jats:p>","DOI":"10.1145\/3372895","type":"journal-article","created":{"date-parts":[[2020,5,4]],"date-time":"2020-05-04T07:56:36Z","timestamp":1588578996000},"page":"1-71","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["A Theory of Slicing for Imperative Probabilistic Programs"],"prefix":"10.1145","volume":"42","author":[{"given":"Torben","family":"Amtoft","sequence":"first","affiliation":[{"name":"Kansas State University, Manhattan, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anindya","family":"Banerjee","sequence":"additional","affiliation":[{"name":"IMDEA Software Institute, Madrid, Spain"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2020,4,17]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2007.10.002"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49630-5_11"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0019410"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2009.10.025"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_6"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676724.2693169"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49674-9_13"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_34"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2011.08.033"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677001"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2593882.2593900"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.peva.2013.11.004"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594303"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-48057-1_24"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49498-1_15"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(81)90036-2"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(85)90012-1"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49665-7_11"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158121"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-47764-0_7"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3156018"},{"key":"e_1_2_1_22_1","volume-title":"Labelled Markov Processes","author":"Panangaden Prakash","unstructured":"Prakash Panangaden. 2009. Labelled Markov Processes. Imperial College Press."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.58784"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1275497.1275502"},{"key":"e_1_2_1_25_1","volume-title":"a Methodology for Language Development. Allyn and Bacon","author":"Schmidt David A.","unstructured":"David A. Schmidt. 1986. Denotational Semantics, a Methodology for Language Development. Allyn and Bacon, Boston."},{"key":"e_1_2_1_26_1","first-page":"121","article-title":"A survey of program slicing techniques","volume":"3","author":"Tip Frank","year":"1995","unstructured":"Frank Tip. 1995. A survey of program slicing techniques. J. Prog. Lang. 3 (1995), 121--189.","journal-title":"J. Prog. Lang."},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1984.5010248"},{"key":"e_1_2_1_29_1","volume-title":"The Formal Semantics of Programming Languages","author":"Winskel Glynn","unstructured":"Glynn Winskel. 1993. The Formal Semantics of Programming Languages. The MIT Press."}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3372895","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3372895","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:13:22Z","timestamp":1750202002000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3372895"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,4,17]]},"references-count":28,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2020,6,30]]}},"alternative-id":["10.1145\/3372895"],"URL":"https:\/\/doi.org\/10.1145\/3372895","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,4,17]]},"assertion":[{"value":"2017-10-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-10-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2020-04-17","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}