{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T11:05:04Z","timestamp":1784199904618,"version":"3.55.0"},"reference-count":64,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2025,6,13]],"date-time":"2025-06-13T00:00:00Z","timestamp":1749772800000},"content-version":"vor","delay-in-days":3,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["2116372,2220408"],"award-info":[{"award-number":["2116372,2220408"]}],"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":[[2025,6,10]]},"abstract":"<jats:p>Exact probabilistic inference is a requirement for many applications of probabilistic programming languages (PPLs) such as in high-consequence settings or verification. However, designing and implementing a PPL with scalable high-performance exact inference is difficult: exact inference engines, much like SAT solvers, are intricate low-level programs that are hard to implement. Due to this implementation challenge, PPLs that support scalable exact inference are restrictive and lack many features of general-purpose languages.<\/jats:p>\n                  <jats:p>This paper presents Roulette, the first discrete probabilistic programming language that combines high-performance exact inference with general-purpose language features. Roulette supports a significant subset of Racket, including data structures, first-class functions, surely-terminating recursion, mutable state, modules, and macros, along with probabilistic features such as finitely supported discrete random variables, conditioning, and top-level inference. The key insight is that there is a close connection between exact probabilistic inference and the symbolic evaluation strategy of Rosette. Building on this connection, Roulette generalizes and extends the Rosette solver-aided programming system to reason about probabilistic rather than symbolic quantities. We prove Roulette sound by generalizing a proof of correctness for Rosette to handle probabilities, and demonstrate its scalability and expressivity on a number of examples.<\/jats:p>","DOI":"10.1145\/3729334","type":"journal-article","created":{"date-parts":[[2025,6,13]],"date-time":"2025-06-13T16:02:27Z","timestamp":1749830547000},"page":"2081-2105","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Roulette: A Language for Expressive, Exact, and Efficient Discrete Probabilistic Programming"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4384-6351","authenticated-orcid":false,"given":"Cameron","family":"Moy","sequence":"first","affiliation":[{"name":"Northeastern University, Boston, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-3242-6969","authenticated-orcid":false,"given":"Jack","family":"Czenszak","sequence":"additional","affiliation":[{"name":"Northeastern University, Boston, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2130-5092","authenticated-orcid":false,"given":"John M.","family":"Li","sequence":"additional","affiliation":[{"name":"Northeastern University, Boston, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7744-4932","authenticated-orcid":false,"given":"Brianna","family":"Marshall","sequence":"additional","affiliation":[{"name":"Northeastern University, Boston, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8190-5412","authenticated-orcid":false,"given":"Steven","family":"Holtzen","sequence":"additional","affiliation":[{"name":"Northeastern University, Boston, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,6,13]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","unstructured":"Michael Ballantyne Mitch Gamburg and Jason Hemann. 2024. Compiled Extensible Multi-language DSLs (Functional Pearl). In International Conference on Functional Programming (ICFP). https:\/\/doi.org\/10.1145\/3674627 10.1145\/3674627","DOI":"10.1145\/3674627"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","unstructured":"Gilles Barthe Boris K\u00f6pf Federico Olmedo and Santiago Zanella Beguelin. 2012. Probabilistic Relational Reasoning for Differential Privacy. In Principles of Programming Languages (POPL). https:\/\/doi.org\/10.1145\/2492061 10.1145\/2492061","DOI":"10.1145\/2492061"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","unstructured":"James Bornholt and Emina Torlak. 2018. Finding Code That Explodes Under Symbolic Evaluation. In Object-Oriented Programming Systems Languages and Applications (OOPSLA). https:\/\/doi.org\/10.1145\/3276519 10.1145\/3276519","DOI":"10.1145\/3276519"},{"key":"e_1_3_2_5_2","unstructured":"William E Byrd. 2009. Relational Programming in miniKanren: Techniques Applications and Implementations. Ph.D. Dissertation. Indiana University."},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","unstructured":"William X Cao Poorva Garg Ryan Tjoa Steven Holtzen Todd Millstein and Guy Van den Broeck. 2023. Scaling Integer Arithmetic in Probabilistic Programs. In Uncertainty in Artificial Intelligence (UAI). https:\/\/doi.org\/10.48550\/arXiv.2307.13837 10.48550\/arXiv.2307.13837","DOI":"10.48550\/arXiv.2307.13837"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","unstructured":"Stephen Chang Alex Knauth and Emina Torlak. 2018. Symbolic Types for Lenient Symbolic Execution. In Principles of Programming Languages (POPL). https:\/\/doi.org\/10.1145\/3158128 10.1145\/3158128","DOI":"10.1145\/3158128"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2007.11.002"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","unstructured":"David Chiang Colin McDonald and Chung-chieh Shan. 2023. Exact Recursive Probabilistic Programming. In Object-Oriented Programming Systems Languages and Applications (OOPSLA). https:\/\/doi.org\/10.1145\/3586050 10.1145\/3586050","DOI":"10.1145\/3586050"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","unstructured":"Arthur Choi Doga Kisa and Adnan Darwiche. 2013. Compiling Probabilistic Graphical Models Using Sentential Decision Diagrams. In Symbolic and Quantitative Approaches to Reasoning with Uncertainty. https:\/\/doi.org\/10.1007\/978-3-642-39091-3_11 10.1007\/978-3-642-39091-3_11","DOI":"10.1007\/978-3-642-39091-3_11"},{"key":"e_1_3_2_11_2","unstructured":"Shumo Chu Chenglong Wang Konstantin Weitz and Alvin Cheung. 2017. Cosette: An Automated Prover for SQL. In Conference on Innovative Data Systems Research (CIDR)."},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","unstructured":"Ryan Culpepper and Andrew Cobb. 2017. Contextual Equivalence for Probabilistic Programs with Continuous Random Variables and Scoring. In European Symposium on Programming (ESOP). https:\/\/doi.org\/10.1007\/978-3-662-54434-1_14 10.1007\/978-3-662-54434-1_14","DOI":"10.1007\/978-3-662-54434-1_14"},{"key":"e_1_3_2_13_2","unstructured":"Adnan Darwiche. 2002. A Compiler for Deterministic Decomposable Negation Normal Form. In AAAI Conference on Artificial Intelligence (AAAI)."},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","unstructured":"Adnan Darwiche. 2011. SDD: A New Canonical Representation of Propositional Knowledge Bases. In International Joint Conference on Artificial Intelligence (IJCAI). https:\/\/doi.org\/10.5591\/978-1-57735-516-8\/IJCAI11-143 10.5591\/978-1-57735-516-8\/IJCAI11-143","DOI":"10.5591\/978-1-57735-516-8\/IJCAI11-143"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1613\/jair.989"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","unstructured":"Leonardo De Moura and Nikolaj Bj\u00f8rner. 2008. Z3: An Efficient SMT Solver. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24 10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_17_2","unstructured":"Luc De Raedt Angelika Kimmig and Hannu Toivonen. 2007. Problog: A Probabilistic Prolog and Its Application in Link Discovery. In International Joint Conference on Artificial Intelligence (IJCAI)."},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068414000076"},{"key":"e_1_3_2_19_2","unstructured":"Matthew Flatt and PLT . 2010. Reference: Racket. Technical Report PLT-TR-2010-1. PLT Design Inc.. https:\/\/racketlang.org\/tr1\/"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.5555\/3267158"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","unstructured":"Norbert Fuhr. 1995. Probabilistic Datalog \u2014 A Logic for Powerful Retrieval Methods. In Conference on Research and Development in Information Retrieval (SIGIR). https:\/\/doi.org\/10.1145\/215206.215372 10.1145\/215206.215372","DOI":"10.1145\/215206.215372"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","unstructured":"Poorva Garg Steven Holtzen Guy Van den Broeck and Todd Millstein. 2024. Bit Blasting Probabilistic Programs. In Programming Language Design and Implementation (PLDI). https:\/\/doi.org\/10.1145\/3656412 10.1145\/3656412","DOI":"10.1145\/3656412"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","unstructured":"Timon Gehr Sasa Misailovic Petar Tsankov Laurent Vanbever Pascal Wiesmann and Martin Vechev. 2018. Bayonet: Probabilistic Inference for Networks. In Programming Language Design and Implementation (PLDI). https:\/\/doi.org\/10.1145\/3296979.3192400 10.1145\/3296979.3192400","DOI":"10.1145\/3296979.3192400"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","unstructured":"Timon Gehr Sasa Misailovic and Martin Vechev. 2016. PSI: Exact Symbolic Inference for Probabilistic Programs. In Computer Aided Verification (CAV). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_4 10.1007\/978-3-319-41528-4_4","DOI":"10.1007\/978-3-319-41528-4_4"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","unstructured":"Timon Gehr Samuel Steffen and Martin T. Vechev. 2020. \ud835\udf06PSI: Exact Inference for Higher-Order Probabilistic Programs. In Programming Language Design and Implementation (PLDI). https:\/\/doi.org\/10.1145\/3385412.3386006 10.1145\/3385412.3386006","DOI":"10.1145\/3385412.3386006"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","unstructured":"Jaco Geldenhuys Matthew B Dwyer and Willem Visser. 2012. Probabilistic Symbolic Execution. In International Symposium on Software Testing and Analysis (ISSTA). https:\/\/doi.org\/10.1145\/2338965.2336773 10.1145\/2338965.2336773","DOI":"10.1145\/2338965.2336773"},{"key":"e_1_3_2_27_2","unstructured":"Jason Hemann and Daniel P. Friedman. 2013. \ud835\udf07Kanren: A Minimal Functional Core for Relational Programming. In Scheme and Functional Programming Workshop."},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","unstructured":"Jason Hemann Daniel P. Friedman William E. Byrd and Matthew Might. 2017. A Simple Complete Search for Logic Programming. In International Conference on Logic Programming (ICLP). https:\/\/doi.org\/10.4230\/OASICS.ICLP.2017.14 10.4230\/OASICS.ICLP.2017.14","DOI":"10.4230\/OASICS.ICLP.2017.14"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1017\/s0956796822000028"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","unstructured":"Steven Holtzen Guy Van den Broeck and Todd Millstein. 2020. Scaling Exact Inference for Discrete Probabilistic Programs. In Object-Oriented Programming Systems Languages and Applications (OOPSLA). https:\/\/doi.org\/10.1145\/3428208 10.1145\/3428208","DOI":"10.1145\/3428208"},{"key":"e_1_3_2_31_2","unstructured":"Steven Holtzen MatthewWang John Gouwar Sam Stites and Minsung Cho. 2025. The Rust Decision Diagram Library (RSDD). https:\/\/github.com\/neuppl\/rsdd"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","unstructured":"Gilles Kahn. 1987. Natural Semantics. In Symposium on Theoretical Aspects of Computer Science (STACS). https:\/\/doi.org\/10.1007\/BFB0039592 10.1007\/BFB0039592","DOI":"10.1007\/BFB0039592"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","unstructured":"Rafael Kiesel and Thomas Eiter. 2023. Knowledge Compilation and More with SharpSAT-TD. In Principles of Knowledge Representation and Reasoning (KR). https:\/\/doi.org\/10.24963\/kr.2023\/40 10.24963\/kr.2023\/40","DOI":"10.24963\/kr.2023\/40"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","unstructured":"Lutz Klinkenberg Christian Blumenthal Mingshuai Chen Darion Haase and Joost-Pieter Katoen. 2024. Exact Bayesian Inference for Loopy Probabilistic Programs using Generating Functions. In Object-Oriented Programming Systems Languages and Applications (OOPSLA). https:\/\/doi.org\/10.1145\/3649844 10.1145\/3649844","DOI":"10.1145\/3649844"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.5555\/1610541"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","unstructured":"Jean-Marie Lagniez and Pierre Marquis. 2017. An Improved Decision-DNNF Compiler. In International Joint Conference on Artificial Intelligence (IJCAI). https:\/\/doi.org\/10.24963\/ijcai.2017\/93 10.24963\/ijcai.2017\/93","DOI":"10.24963\/ijcai.2017\/93"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","unstructured":"Cameron Moy Jack Czenszak John M. Li Brianna Marshall and Steven Holtzen. 2025. Artifact: Roulette. https:\/\/doi.org\/10.5281\/zenodo.15253254 10.5281\/zenodo.15253254","DOI":"10.5281\/zenodo.15253254"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","unstructured":"Christian Muise Sheila McIlraith J Christopher Beck and Eric Hsu. 2012. Dsharp: Fast d-DNNF Compilation with sharpSAT. In Advances in Artificial Intelligence. https:\/\/doi.org\/10.1007\/978-3-642-30353-1_36 10.1007\/978-3-642-30353-1_36","DOI":"10.1007\/978-3-642-30353-1_36"},{"key":"e_1_3_2_39_2","unstructured":"Lawrence Murray Daniel Lund\u00e9n Jan Kudlicka David Broman and Thomas Sch\u00f6n. 2018. Delayed Sampling and Automatic Rao-Blackwellization of Probabilistic Programs. In International Conference on Artificial Intelligence and Statistics."},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","unstructured":"Praveen Narayanan Jacques Carette Wren Romano Chung-chieh Shan and Robert Zinkov. 2016. Probabilistic Inference by Program Transformation in Hakaru (System Description). In Functional and Logic Programming (FLOPS). https:\/\/doi.org\/10.1007\/978-3-319-29604-3_5 10.1007\/978-3-319-29604-3_5","DOI":"10.1007\/978-3-319-29604-3_5"},{"key":"e_1_3_2_41_2","unstructured":"Luke Nelson Jacob Van Geffen Emina Torlak and Xi Wang. 2020. Specification and Verification in the Field: Applying Formal Methods to BPF Just-in-Time Compilers in the Linux Kernel. In Operating Systems Design and Implementation (OSDI)."},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90061-J"},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","unstructured":"Lisa Oakley Steven Holtzen and Alina Oprea. 2024. Synthesizing Tight Privacy and Accuracy Bounds via Weighted Model Counting. In Computer Security Foundations Symposium (CSF). https:\/\/doi.org\/10.1109\/CSF61375.2024.00048 10.1109\/CSF61375.2024.00048","DOI":"10.1109\/CSF61375.2024.00048"},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","unstructured":"Scott Owens Magnus O. Myreen Ramana Kumar and Yong Kiam Tan. 2016. Functional Big-Step Semantics. In European Symposium on Programming (ESOP). https:\/\/doi.org\/10.1007\/978-3-662-49498-1_23 10.1007\/978-3-662-49498-1_23","DOI":"10.1007\/978-3-662-49498-1_23"},{"key":"e_1_3_2_45_2","unstructured":"Umut Oztok Arthur Choi and Adnan Darwiche. 2016. Solving PPPP-Complete Problems using Knowledge Compilation. In Principles of Knowledge Representation and Reasoning (KR)."},{"key":"e_1_3_2_46_2","unstructured":"Umut Oztok and Adnan Darwiche. 2015. A Top-Down Compiler for Sentential Decision Diagrams. In International Joint Conference on Artificial Intelligence (IJCAI)."},{"key":"e_1_3_2_47_2","doi-asserted-by":"publisher","DOI":"10.1613\/jair.1.11201"},{"key":"e_1_3_2_48_2","unstructured":"Judea Pearl. 1985. Bayesian Networks: A Model of Self-Activated Memory for Evidential Reasoning. In Conference of the Cognitive Science Society."},{"key":"e_1_3_2_49_2","doi-asserted-by":"publisher","unstructured":"Stuart Pernsteiner Calvin Loncaric Emina Torlak Zachary Tatlock Xi Wang Michael D. Ernst and Jonathan Jacky. 2016. Investigating Safety of a Radiotherapy Machine Using System Models with Pluggable Checkers. In Computer Aided Verification (CAV). https:\/\/doi.org\/10.1007\/978-3-319-41540-6_2 10.1007\/978-3-319-41540-6_2","DOI":"10.1007\/978-3-319-41540-6_2"},{"key":"e_1_3_2_50_2","doi-asserted-by":"publisher","unstructured":"Phitchaya Mangpo Phothilimthana Aditya Thakur Rastislav Bod\u00edk and Dinakar Dhurjati. 2016. Scaling up Superoptimization. In Architectural Support for Programming Languages and Operating Systems (ASPLOS). https:\/\/doi.org\/10.1145\/2872362.2872387 10.1145\/2872362.2872387","DOI":"10.1145\/2872362.2872387"},{"key":"e_1_3_2_51_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139084673"},{"key":"e_1_3_2_52_2","doi-asserted-by":"publisher","unstructured":"Sorawee Porncharoenwase James Bornholt and Emina Torlak. 2020. Fixing Code That Explodes Under Symbolic Evaluation. In Verification Model Checking and Abstract Interpretation (VMCAI). https:\/\/doi.org\/10.1007\/978-3-030-39322-9_3 10.1007\/978-3-030-39322-9_3","DOI":"10.1007\/978-3-030-39322-9_3"},{"key":"e_1_3_2_53_2","doi-asserted-by":"publisher","unstructured":"Sorawee Porncharoenwase Luke Nelson Xi Wang and Emina Torlak. 2022. A Formal Foundation for Symbolic Evaluation with Merging. In Principles of Programming Languages (POPL). https:\/\/doi.org\/10.1145\/3498709 10.1145\/3498709","DOI":"10.1145\/3498709"},{"key":"e_1_3_2_54_2","doi-asserted-by":"publisher","DOI":"10.1109\/5.18626"},{"key":"e_1_3_2_55_2","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(94)00092-1"},{"key":"e_1_3_2_56_2","doi-asserted-by":"publisher","DOI":"10.1016\/0096-0551(89)90004-0"},{"key":"e_1_3_2_57_2","doi-asserted-by":"publisher","unstructured":"Feras A Saad Martin C Rinard and Vikash K Mansinghka. 2021. SPPL: Probabilistic Programming with Fast Exact Symbolic Inference. In Programming Language Design and Implementation (PLDI). https:\/\/doi.org\/10.1145\/3453483.3454078 10.1145\/3453483.3454078","DOI":"10.1145\/3453483.3454078"},{"key":"e_1_3_2_58_2","unstructured":"Tian Sang Paul Beame and Henry A Kautz. 2005. Performing Bayesian Inference by Weighted Model Counting. In AAAI Conference on Artificial Intelligence (AAAI)."},{"key":"e_1_3_2_59_2","doi-asserted-by":"publisher","unstructured":"Steffen Smolka Praveen Kumar David M. Kahn Nate Foster Justin Hsu Dexter Kozen and Alexandra Silva. 2019. Scalable Verification of Probabilistic Networks. In Programming Language Design and Implementation (PLDI). https:\/\/doi.org\/10.1145\/3314221.3314639 10.1145\/3314221.3314639","DOI":"10.1145\/3314221.3314639"},{"key":"e_1_3_2_60_2","unstructured":"Fabio Somenzi. 1998. CUDD: CU Decision Diagram Package Release. https:\/\/add-lib.scce.info\/assets\/documents\/cuddmanual.pdf"},{"key":"e_1_3_2_61_2","doi-asserted-by":"publisher","unstructured":"Zachary Susag Sumit Lahiri Justin Hsu and Subhajit Roy. 2022. Symbolic Execution for Randomized Programs. In Object-Oriented Programming Systems Languages and Applications (OOPSLA). https:\/\/doi.org\/10.1145\/3563344 10.1145\/3563344","DOI":"10.1145\/3563344"},{"key":"e_1_3_2_62_2","doi-asserted-by":"publisher","unstructured":"Emina Torlak and Rastislav Bodik. 2013. Growing Solver-Aided Languages with Rosette. In Onward!. https:\/\/doi.org\/10.1145\/2509578.2509586 10.1145\/2509578.2509586","DOI":"10.1145\/2509578.2509586"},{"key":"e_1_3_2_63_2","doi-asserted-by":"publisher","unstructured":"Emina Torlak and Rastislav Bod\u00edk. 2014. A Lightweight Symbolic Virtual Machine for Solver-Aided Host Languages. In Programming Language Design and Implementation (PLDI). https:\/\/doi.org\/10.1145\/2594291.2594340 10.1145\/2594291.2594340","DOI":"10.1145\/2594291.2594340"},{"key":"e_1_3_2_64_2","doi-asserted-by":"publisher","unstructured":"Erik Voogd Einar Broch Johnsen Alexandra Silva Zachary J Susag and Andrzej W\u0105sowski. 2023. Symbolic Semantics for Probabilistic Programs. In International Conference on Quantitative Evaluation of Systems. https:\/\/doi.org\/10.1007\/978-3-031-43835-6_23 10.1007\/978-3-031-43835-6_23","DOI":"10.1007\/978-3-031-43835-6_23"},{"key":"e_1_3_2_65_2","doi-asserted-by":"publisher","unstructured":"Konstantin Weitz Doug Woos Emina Torlak Michael D. Ernst Arvind Krishnamurthy and Zachary Tatlock. 2016. Scalable Verification of Border Gateway Protocol Configurations with an SMT Solver. In Object-Oriented Programming Systems Languages and Applications (OOPSLA). https:\/\/doi.org\/10.1145\/2983990.2984012 10.1145\/2983990.2984012","DOI":"10.1145\/2983990.2984012"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3729334","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3729334","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T10:05:16Z","timestamp":1784196316000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3729334"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,10]]},"references-count":64,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2025,6,10]]}},"alternative-id":["10.1145\/3729334"],"URL":"https:\/\/doi.org\/10.1145\/3729334","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,6,10]]},"assertion":[{"value":"2024-11-15","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-03-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-06-13","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}