{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T09:06:57Z","timestamp":1770282417698,"version":"3.49.0"},"reference-count":72,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,1,2]],"date-time":"2019-01-02T00:00:00Z","timestamp":1546387200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1566015, 1704117, 1652140, 1637532"],"award-info":[{"award-number":["1566015, 1704117, 1652140, 1637532"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2019,1,2]]},"abstract":"<jats:p>We propose trace abstraction modulo probability, a proof technique for verifying high-probability accuracy guarantees of probabilistic programs. Our proofs overapproximate the set of program traces using failure automata, finite-state automata that upper bound the probability of failing to satisfy a target specification. We automate proof construction by reducing probabilistic reasoning to logical reasoning: we use program synthesis methods to select axioms for sampling instructions, and then apply Craig interpolation to prove that traces fail the target specification with only a small probability. Our method handles programs with unknown inputs, parameterized distributions, infinite state spaces, and parameterized specifications. We evaluate our technique on a range of randomized algorithms drawn from the differential privacy literature and beyond. To our knowledge, our approach is the first to automatically establish accuracy properties of these algorithms.<\/jats:p>","DOI":"10.1145\/3290352","type":"journal-article","created":{"date-parts":[[2019,1,4]],"date-time":"2019-01-04T13:33:51Z","timestamp":1546608831000},"page":"1-31","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":16,"title":["Trace abstraction modulo probability"],"prefix":"10.1145","volume":"3","author":[{"given":"Calvin","family":"Smith","sequence":"first","affiliation":[{"name":"University of Wisconsin-Madison, USA"}]},{"given":"Justin","family":"Hsu","sequence":"additional","affiliation":[{"name":"University of Wisconsin-Madison, USA"}]},{"given":"Aws","family":"Albarghouthi","sequence":"additional","affiliation":[{"name":"University of Wisconsin-Madison, USA"}]}],"member":"320","published-online":{"date-parts":[[2019,1,2]]},"reference":[{"key":"e_1_2_2_2_1","volume-title":"Probabilistic Horn Clause Verification. In International Symposium on Static Analysis (SAS)","author":"Albarghouthi Aws","year":"2017"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133904"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27940-9_4"},{"key":"e_1_2_2_5_1","volume-title":"Constraint-Based Synthesis of Coupling Proofs. In International Conference on Computer Aided Verification (CAV)","author":"Albarghouthi Aws","year":"2018"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158146"},{"key":"e_1_2_2_7_1","volume-title":"International Conference on Computer Aided Verification (CAV)","author":"Albarghouthi Aws"},{"key":"e_1_2_2_8_1","volume-title":"Handbook of Model Checking","author":"Baier Christel"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/380921.380932"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4_3"},{"key":"e_1_2_2_11_1","volume-title":"An AssertionBased Program Logic for Probabilistic Programs. In European Symposium on Programming (ESOP)","author":"Barthe Gilles","year":"2018"},{"key":"e_1_2_2_12_1","first-page":"1","article-title":"A Program Logic for Union Bounds. In International Colloquium on Automata, Languages and Programming (ICALP), Rome","volume":"107","author":"Barthe Gilles","year":"2016","journal-title":"Italy."},{"key":"e_1_2_2_13_1","volume-title":"International Joint Conference on Artificial Intelligence (IJCAI)","author":"Belle Vaishak","year":"2015"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1162\/153244302760200704"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509546"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2007.02.040"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_34"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2043621.2043626"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4_1"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837639"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009873"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_26"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-016-9365-5"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_7"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491411.2491423"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/11547662_8"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_9"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.2307\/2963594"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192399"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_31"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2090236.2090255"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/11681878_14"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806689.1806787"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1561\/0400000042"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429086"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192400"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4_4"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.5555\/647766.733618"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3035918.3035940"},{"key":"e_1_2_2_42_1","volume-title":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"Heizmann Matthias","year":"2018"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03237-0_7"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706353"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_2"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964021"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_16"},{"key":"e_1_2_2_48_1","volume-title":"Efficient Interpolation for the Theory of Arrays. In International Joint Conference on Artificial Intelligence (IJCAI)","volume":"10900","author":"Hoenicke Jochen","year":"2018"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3187009.3177733"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2934574"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-93900-9_17"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-010-0097-6"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(85)90012-1"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1109\/ALLERTON.2010.5707120"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.5555\/2032305.2032352"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1017584715408"},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2011.15"},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158121"},{"key":"e_1_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45069-6_1"},{"key":"e_1_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_14"},{"key":"e_1_2_2_61_1","doi-asserted-by":"publisher","DOI":"10.1109\/FOCS.2007.41"},{"key":"e_1_2_2_62_1","doi-asserted-by":"publisher","DOI":"10.5555\/647169.718164"},{"key":"e_1_2_2_63_1","doi-asserted-by":"publisher","DOI":"10.5555\/645395.651948"},{"key":"e_1_2_2_64_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2005.02.008"},{"key":"e_1_2_2_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/229542.229547"},{"key":"e_1_2_2_66_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-29604-3_5"},{"key":"e_1_2_2_67_1","volume-title":"VPHL: A Verified Partial-Correctness Logic for Probabilistic Programs. In Conference on the Mathematical Foundations of Programming Semantics (MFPS)","author":"Rand Robert","year":"2015"},{"key":"e_1_2_2_68_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54108-7_1"},{"key":"e_1_2_2_69_1","volume-title":"Formal Methods in Computer-Aided Design (FMCAD)","author":"Rummer Philipp"},{"key":"e_1_2_2_70_1","unstructured":"C. Smith J. Hsu and A. Albarghouthi. 2018. Trace Abstraction Modulo Probability. ArXiv e-prints (Oct. 2018). arXiv: cs.PL\/1810.12396  C. Smith J. Hsu and A. Albarghouthi. 2018. Trace Abstraction Modulo Probability. ArXiv e-prints (Oct. 2018). arXiv: cs.PL\/1810.12396"},{"key":"e_1_2_2_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009864"},{"key":"e_1_2_2_72_1","doi-asserted-by":"publisher","DOI":"10.5555\/1987389.1987407"},{"key":"e_1_2_2_73_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192408"},{"key":"e_1_2_2_74_1","doi-asserted-by":"publisher","DOI":"10.1080\/01621459.1965.10480775"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290352","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3290352","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3290352","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:58:04Z","timestamp":1750208284000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290352"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,2]]},"references-count":72,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2019,1,2]]}},"alternative-id":["10.1145\/3290352"],"URL":"https:\/\/doi.org\/10.1145\/3290352","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,1,2]]},"assertion":[{"value":"2019-01-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}