{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T20:16:03Z","timestamp":1784837763036,"version":"3.55.0"},"publisher-location":"Cham","reference-count":58,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032227225","type":"print"},{"value":"9783032227232","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>This paper focuses on effective user diagnostics generated during the deductive verification of probabilistic programs. Our key principle is based on providing slices for (1) error reporting, (2) proof simplification, and (3) preserving successful verification results. By formally defining these different notions on HeyVL, an existing quantitative intermediate verification language (IVL), our concepts (and implementation) can be used to obtain diagnostics for a range of probabilistic programming languages. Slicing for error reporting is a novel notion of error localization for quantitative assertions. We demonstrate slicing-based diagnostics on a variety of proof rules such as quantitative versions of the specification statement and invariant-based loop rules, and formally prove the correctness of specialized error messages and verification hints.<\/jats:p>\n                  <jats:p>\n                    We implemented our user diagnostics into the deductive verifier Caesar. Our novel implementation \u2014 called\n                    <jats:italic>Brutus<\/jats:italic>\n                    \u2014 can search for slices which do or do not verify, corresponding to each of the three diagnostic notions. For error reporting (1), it exploits a binary search-based algorithm that minimizes error-witnessing slices. To solve for slices that verify (2 and 3), we empirically compare different algorithms based on unsatisfiable cores, minimal unsatisfiable subset enumeration, and a direct SMT encoding of the slicing problem. Our empirical evaluation of Brutus on existing and new benchmarks shows that we can find slices that are both small and informative.\n                  <\/jats:p>","DOI":"10.1007\/978-3-032-22723-2_8","type":"book-chapter","created":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T12:00:52Z","timestamp":1775822452000},"page":"210-240","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Error Localization, Certificates, and Hints for Probabilistic Program Verification via Slicing"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4329-530X","authenticated-orcid":false,"given":"Philipp","family":"Schr\u00f6er","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5664-6773","authenticated-orcid":false,"given":"Darion","family":"Haase","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6143-1926","authenticated-orcid":false,"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,4,10]]},"reference":[{"key":"8_CR1","doi-asserted-by":"publisher","unstructured":"E. \u00c1brah\u00e1m, B. Becker, C. Dehnert, N. Jansen, J. Katoen, and R. Wimmer: Counterexample Generation for Discrete-Time Markov Models: An Introductory Survey. In: M. Bernardo, F. Damiani, R. H\u00e4hnle, E.B. Johnsen, and I. Schaefer. Formal Methods for Executable Software Models - 14th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM 2014, Bertinoro, Italy, June 16-20, 2014, Advanced Lectures. LNCS, vol. 8483, pp. 65\u2013121. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-319-07317-0_3","DOI":"10.1007\/978-3-319-07317-0_3"},{"key":"8_CR2","doi-asserted-by":"crossref","unstructured":"W. Ahrendt, B. Beckert, R. Bubel, R. H\u00e4hnle, P.H. Schmitt, and M. Ulbrich: Deductive Software Verification - The KeY Book - From Theory to Practice. Springer (2016)","DOI":"10.1007\/978-3-319-49812-6"},{"key":"8_CR3","doi-asserted-by":"publisher","unstructured":"T. Amtoft and A. Banerjee: A Theory of Slicing for Imperative Probabilistic Programs. ACM Trans. Program. Lang. Syst. 42(2), 6:1\u20136:71 (2020). https:\/\/doi.org\/10.1145\/3372895","DOI":"10.1145\/3372895"},{"key":"8_CR4","doi-asserted-by":"publisher","unstructured":"T. Amtoft and A. Banerjee: A Theory of Slicing for Probabilistic Control Flow Graphs. In: B. Jacobs and C. L\u00f6ding. Foundations of Software Science and Computation Structures - 19th International Conference, FOSSACS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings. LNCS, vol. 9634, pp. 180\u2013196. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49630-5_11","DOI":"10.1007\/978-3-662-49630-5_11"},{"key":"8_CR5","doi-asserted-by":"publisher","unstructured":"C. Andrieu, N. de Freitas, A. Doucet, and M.I. Jordan: An Introduction to MCMC for Machine Learning. Mach. Learn. 50(1-2), 5\u201343 (2003). https:\/\/doi.org\/10.1023\/A:1020281327116","DOI":"10.1023\/A:1020281327116"},{"key":"8_CR6","doi-asserted-by":"publisher","unstructured":"V. Astrauskas, A. B\u00edl\u00fd, J. Fiala, Z. Grannan, C. Matheja, P. M\u00fcller, F. Poli, and A.J. Summers: The Prusti Project: Formal Verification for Rust. In: J.V. Deshmukh, K. Havelund, and I. Perez. NASA Formal Methods - 14th International Symposium, NFM 2022, Pasadena, CA, USA, May 24-27, 2022, Proceedings. LNCS, vol. 13260, pp. 88\u2013108. Springer, Heidelberg (2022). https:\/\/doi.org\/10.1007\/978-3-031-06773-0_5","DOI":"10.1007\/978-3-031-06773-0_5"},{"key":"8_CR7","doi-asserted-by":"publisher","unstructured":"J.B. Barros, D.C. da Cruz, P.R. Henriques, and J.S. Pinto: Assertion-based Slicing and Slice Graphs. In: J.L. Fiadeiro, S. Gnesi, and A. Maggiolo-Schettini. 8th IEEE International Conference on Software Engineering and Formal Methods, SEFM 2010, Pisa, Italy, 13-18 September 2010, pp. 93\u2013102. IEEE Computer Society (2010). https:\/\/doi.org\/10.1109\/SEFM.2010.18","DOI":"10.1109\/SEFM.2010.18"},{"key":"8_CR8","doi-asserted-by":"publisher","unstructured":"J.B. Barros, D.C. da Cruz, P.R. Henriques, and J.S. Pinto: Assertion-based slicing and slice graphs. Formal Aspects Comput. 24(2), 217\u2013248 (2012). https:\/\/doi.org\/10.1007\/S00165-011-0196-1","DOI":"10.1007\/S00165-011-0196-1"},{"key":"8_CR9","doi-asserted-by":"publisher","unstructured":"K. Batz, M. Chen, B.L. Kaminski, J. Katoen, C. Matheja, and P. Schr\u00f6er: Latticed k-Induction with an Application to Probabilistic Programs. In: A. Silva and K.R.M. Leino. Computer Aided Verification - 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part II. LNCS, vol. 12760, pp. 524\u2013549. Springer, Heidelberg (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_25","DOI":"10.1007\/978-3-030-81688-9_25"},{"key":"8_CR10","doi-asserted-by":"publisher","unstructured":"K. Batz, B.L. Kaminski, J. Katoen, and C. Matheja: Relatively complete verification of probabilistic programs: an expressive language for expectation-based reasoning. Proc. ACM Program. Lang. 5(POPL), 1\u201330 (2021). https:\/\/doi.org\/10.1145\/3434320","DOI":"10.1145\/3434320"},{"key":"8_CR11","doi-asserted-by":"publisher","unstructured":"K. Batz, J. Katoen, F. Randone, and T. Winkler: Foundations for Deductive Verification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Back. Proc. ACM Program. Lang. 9(OOPSLA1), 421\u2013448 (2025). https:\/\/doi.org\/10.1145\/3720429","DOI":"10.1145\/3720429"},{"key":"8_CR12","unstructured":"E. Bingham, J.P. Chen, M. Jankowiak, F. Obermeyer, N. Pradhan, T. Karaletsos, R. Singh, P.A. Szerlip, P. Horsfall, and N.D. Goodman: Pyro: Deep Universal Probabilistic Programming. J. Mach. Learn. Res. 20, 28:1\u201328:6 (2019)"},{"key":"8_CR13","doi-asserted-by":"publisher","unstructured":"B. Carpenter, A. Gelman, M.D. Hoffman, D. Lee, B. Goodrich, M. Betancourt, M. Brubaker, J. Guo, P. Li, and A. Riddell: Stan: A Probabilistic Programming Language. Journal of Statistical Software 76(1), 1\u201332 (2017). https:\/\/doi.org\/10.18637\/jss.v076.i01","DOI":"10.18637\/jss.v076.i01"},{"key":"8_CR14","doi-asserted-by":"publisher","unstructured":"A. Chakarov and S. Sankaranarayanan: Probabilistic Program Analysis with Martingales. In: N. Sharygina and H. Veith. Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings. LNCS, vol. 8044, pp. 511\u2013526. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_34","DOI":"10.1007\/978-3-642-39799-8_34"},{"key":"8_CR15","doi-asserted-by":"publisher","unstructured":"K. Chatterjee, A.K. Goharshady, T. Meggendorfer, and D. Zikelic: Quantitative Bounds on Resource Usage of Probabilistic Programs. Proc. ACM Program. Lang. 8(OOPSLA1), 362\u2013391 (2024). https:\/\/doi.org\/10.1145\/3649824","DOI":"10.1145\/3649824"},{"key":"8_CR16","unstructured":"P. Cousot: Principles of Abstract Interpretation. The MIT Press (2021)"},{"key":"8_CR17","doi-asserted-by":"publisher","unstructured":"S. Dailler, D. Hauzar, C. March\u00e9, and Y. Moy: Instrumenting a weakest precondition calculus for counterexample generation. J. Log. Algebraic Methods Program. 99, 97\u2013113 (2018). https:\/\/doi.org\/10.1016\/J.JLAMP.2018.05.003","DOI":"10.1016\/J.JLAMP.2018.05.003"},{"key":"8_CR18","doi-asserted-by":"crossref","unstructured":"L. De Moura and N. Bj\u00f8rner: Z3: an efficient SMT solver. In: Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. TACAS\u201908\/ETAPS\u201908, pp. 337\u2013340. Springer-Verlag, Budapest, Hungary (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"8_CR19","doi-asserted-by":"publisher","unstructured":"C. Dehnert, N. Jansen, R. Wimmer, E. \u00c1brah\u00e1m, and J. Katoen: Fast Debugging of PRISM Models. In: F. Cassez and J. Raskin. Automated Technology for Verification and Analysis - 12th International Symposium, ATVA 2014, Sydney, NSW, Australia, November 3-7, 2014, Proceedings. LNCS, vol. 8837, pp. 146\u2013162. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-319-11936-6_11","DOI":"10.1007\/978-3-319-11936-6_11"},{"key":"8_CR20","doi-asserted-by":"publisher","unstructured":"T. Gehr, S. Misailovic, P. Tsankov, L. Vanbever, P. Wiesmann, and M.T. Vechev: Bayonet: probabilistic inference for networks. In: J.S. Foster and D. Grossman. Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018, Philadelphia, PA, USA, June 18-22, 2018, pp. 586\u2013602. ACM (2018). https:\/\/doi.org\/10.1145\/3192366.3192400","DOI":"10.1145\/3192366.3192400"},{"key":"8_CR21","doi-asserted-by":"publisher","unstructured":"R. H\u00e4hnle: Dijkstra\u2019s Legacy on Program Verification. In: Edsger Wybe Dijkstra: His Life, Work, and Legacy. Ed. by K.R. Apt and T. Hoare, pp. 105\u2013140. ACM \/ Morgan & Claypool (2022). https:\/\/doi.org\/10.1145\/3544585.3544593","DOI":"10.1145\/3544585.3544593"},{"key":"8_CR22","doi-asserted-by":"publisher","unstructured":"T. Han and J. Katoen: Counterexamples in Probabilistic Model Checking. In: O. Grumberg and M. Huth. Tools and Algorithms for the Construction and Analysis of Systems, 13th International Conference, TACAS 2007, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007 Braga, Portugal, March 24 - April 1, 2007, Proceedings. LNCS, vol. 4424, pp. 72\u201386. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-71209-1_8","DOI":"10.1007\/978-3-540-71209-1_8"},{"key":"8_CR23","doi-asserted-by":"publisher","unstructured":"S. Holtzen, G.V. den Broeck, and T.D. Millstein: Scaling exact inference for discrete probabilistic programs. Proc. ACM Program. Lang. 4(OOPSLA), 140:1\u2013140:31 (2020). https:\/\/doi.org\/10.1145\/3428208","DOI":"10.1145\/3428208"},{"key":"8_CR24","doi-asserted-by":"publisher","unstructured":"C. Hur, A.V. Nori, S.K. Rajamani, and S. Samuel: Slicing probabilistic programs. In: M.F.P. O\u2019Boyle and K. Pingali. ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI \u201914, Edinburgh, United Kingdom - June 09 - 11, 2014, pp. 133\u2013144. ACM (2014). https:\/\/doi.org\/10.1145\/2594291.2594303","DOI":"10.1145\/2594291.2594303"},{"key":"8_CR25","unstructured":"N. Jansen: Counterexamples in probabilistic verification. PhD thesis, RWTH Aachen University, Germany (2015)."},{"key":"8_CR26","doi-asserted-by":"publisher","unstructured":"N. Jansen, B.L. Kaminski, J. Katoen, F. Olmedo, F. Gretz, and A. McIver: Conditioning in Probabilistic Programming. In: D.R. Ghica. The 31st Conference on the Mathematical Foundations of Programming Semantics, MFPS 2015, Nijmegen, The Netherlands, June 22-25, 2015. Electronic Notes in Theoretical Computer Science, pp. 199\u2013216. Elsevier (2015). https:\/\/doi.org\/10.1016\/j.entcs.2015.12.013","DOI":"10.1016\/j.entcs.2015.12.013"},{"key":"8_CR27","doi-asserted-by":"publisher","unstructured":"S. Jantsch, H. Harder, F. Funke, and C. Baier: Switss: Computing Small Witnessing Subsystems. In: 2020 Formal Methods in Computer Aided Design, FMCAD 2020, Haifa, Israel, September 21-24, 2020, pp. 236\u2013244. IEEE (2020). https:\/\/doi.org\/10.34727\/2020\/ISBN.978-3-85448-042-6_31","DOI":"10.34727\/2020\/ISBN.978-3-85448-042-6_31"},{"key":"8_CR28","unstructured":"B.L. Kaminski: Advanced weakest precondition calculi for probabilistic programs. PhD thesis, RWTH Aachen University, Germany (2019)."},{"key":"8_CR29","doi-asserted-by":"publisher","unstructured":"B.L. Kaminski and J. Katoen: On the Hardness of Almost-Sure Termination. In: G.F. Italiano, G. Pighizzini, and D. Sannella. Mathematical Foundations of Computer Science 2015 - 40th International Symposium, MFCS 2015, Milan, Italy, August 24-28, 2015, Proceedings, Part I. LNCS, vol. 9234, pp. 307\u2013318. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-48057-1_24","DOI":"10.1007\/978-3-662-48057-1_24"},{"key":"8_CR30","doi-asserted-by":"publisher","unstructured":"B.L. Kaminski, J. Katoen, C. Matheja, and F. Olmedo: Weakest Precondition Reasoning for Expected Runtimes of Randomized Algorithms. J. ACM 65(5), 30:1\u201330:68 (2018). https:\/\/doi.org\/10.1145\/3208102","DOI":"10.1145\/3208102"},{"key":"8_CR31","doi-asserted-by":"publisher","unstructured":"J. L\u00e9chenet, N. Kosmatov, and P.L. Gall: Cut branches before looking for bugs: certifiably sound verification on relaxed slices. Formal Aspects Comput. 30(1), 107\u2013131 (2018). https:\/\/doi.org\/10.1007\/S00165-017-0439-X","DOI":"10.1007\/S00165-017-0439-X"},{"key":"8_CR32","doi-asserted-by":"publisher","unstructured":"K.R.M. Leino: Dafny: An Automatic Program Verifier for Functional Correctness. In: E.M. Clarke and A. Voronkov. Logic for Programming, Artificial Intelligence, and Reasoning - 16th International Conference, LPAR-16, Dakar, Senegal, April 25-May 1, 2010, Revised Selected Papers. LNCS, vol. 6355, pp. 348\u2013370. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-17511-4_20","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"8_CR33","unstructured":"K.R.M. Leino: This is Boogie 2, (2008). https:\/\/www.microsoft.com\/en-us\/research\/publication\/this-is-boogie-2-2\/"},{"key":"8_CR34","doi-asserted-by":"crossref","unstructured":"K.R.M. Leino, T.D. Millstein, and J.B. Saxe: Generating error traces from verification-condition counterexamples. Sci. Comput. Program. 55(1-3), 209\u2013226 (2005)","DOI":"10.1016\/j.scico.2004.05.016"},{"key":"8_CR35","doi-asserted-by":"publisher","unstructured":"M.H. Liffiton and A. Malik: Enumerating Infeasibility: Finding Multiple MUSes Quickly. In: C.P. Gomes and M. Sellmann. Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems, 10th International Conference, CPAIOR 2013, Yorktown Heights, NY, USA, May 18-22, 2013. Proceedings. LNCS, vol. 7874, pp. 160\u2013175. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38171-3_11","DOI":"10.1007\/978-3-642-38171-3_11"},{"key":"8_CR36","unstructured":"T. Liu: Efficient Verification of Programs with Complex Data Structures Using SMT Solvers. PhD thesis, Karlsruhe Institute of Technology, Germany (2018)."},{"key":"8_CR37","doi-asserted-by":"publisher","unstructured":"R. Majumdar and V.R. Sathiyanarayana: Sound and Complete Proof Rules for Probabilistic Termination. Proc. ACM Program. Lang. 9(POPL), 1871\u20131902 (2025). https:\/\/doi.org\/10.1145\/3704899","DOI":"10.1145\/3704899"},{"key":"8_CR38","doi-asserted-by":"crossref","unstructured":"A. McIver and C. Morgan: Abstraction, Refinement and Proof for Probabilistic Systems. Springer (2005)","DOI":"10.1145\/1059816.1059824"},{"key":"8_CR39","unstructured":"Microsoft: Language Server Protocol Specification - 3.17, (2024). https:\/\/microsoft.github.io\/language-server-protocol\/specifications\/lsp\/3.17\/specification\/ (visited on 09\/09\/2024)"},{"key":"8_CR40","doi-asserted-by":"publisher","unstructured":"M. Moosbrugger, M. Stankovic, E. Bartocci, and L. Kov\u00e1cs: This is the moment for probabilistic loops. Proc. ACM Program. Lang. 6(OOPSLA2), 1497\u20131525 (2022). https:\/\/doi.org\/10.1145\/3563341","DOI":"10.1145\/3563341"},{"key":"8_CR41","doi-asserted-by":"publisher","unstructured":"C. Morgan: The Specification Statement. ACM Trans. Program. Lang. Syst. 10(3), 403\u2013419 (1988). https:\/\/doi.org\/10.1145\/44501.44503","DOI":"10.1145\/44501.44503"},{"key":"8_CR42","unstructured":"P. M\u00fcller: Building Deductive Program Verifiers, (2018). https:\/\/pmpub.inf.ethz.ch\/publications\/Mueller19.pdf"},{"key":"8_CR43","doi-asserted-by":"publisher","unstructured":"P. M\u00fcller, M. Schwerhoff, and A.J. Summers: Viper: A Verification Infrastructure for Permission-Based Reasoning. In: B. Jobstmann and K.R.M. Leino. Verification, Model Checking, and Abstract Interpretation - 17th International Conference, VMCAI 2016, St. Petersburg, FL, USA, January 17-19, 2016. Proceedings. LNCS, vol. 9583, pp. 41\u201362. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49122-5_3","DOI":"10.1007\/978-3-662-49122-5_3"},{"key":"8_CR44","doi-asserted-by":"publisher","unstructured":"M. Navarro and F. Olmedo: Slicing of probabilistic programs based on specifications. Sci. Comput. Program. 220, 102822 (2022). https:\/\/doi.org\/10.1016\/J.SCICO.2022.102822","DOI":"10.1016\/J.SCICO.2022.102822"},{"key":"8_CR45","doi-asserted-by":"publisher","unstructured":"F. Olmedo: Slicing of Probabilistic Programs: A Review of Existing Approaches. ACM Comput. Surv. 58(3) (2025). https:\/\/doi.org\/10.1145\/3764581","DOI":"10.1145\/3764581"},{"key":"8_CR46","doi-asserted-by":"publisher","unstructured":"F. Olmedo: Static Slicing for Probabilistic Programs: An Overview. In: Principles of Verification: Cycling the Probabilistic Landscape: Essays Dedicated to Joost-Pieter Katoen on the Occasion of His 60th Birthday, Part I, pp. 155\u2013178. Springer Nature Switzerland, Cham (2025). https:\/\/doi.org\/10.1007\/978-3-031-75783-9_7","DOI":"10.1007\/978-3-031-75783-9_7"},{"key":"8_CR47","unstructured":"D. Park: Fixpoint Induction and Proofs of Program Properties. Machine Intelligence 5 (1969)"},{"key":"8_CR48","doi-asserted-by":"publisher","unstructured":"J.N. Ruskiewicz: Localizing and Understanding Verification Errors. PhD thesis, ETH Zurich, Z\u00fcrich, Switzerland (2012). https:\/\/doi.org\/10.3929\/ETHZ-A-007326234","DOI":"10.3929\/ETHZ-A-007326234"},{"key":"8_CR49","doi-asserted-by":"publisher","unstructured":"P. Schr\u00f6er, K. Batz, B.L. Kaminski, J. Katoen, and C. Matheja: A Deductive Verification Infrastructure for Probabilistic Programs. Proc. ACM Program. Lang. 7(OOPSLA2), 2052\u20132082 (2023). https:\/\/doi.org\/10.1145\/3622870","DOI":"10.1145\/3622870"},{"key":"8_CR50","doi-asserted-by":"crossref","unstructured":"P. Schr\u00f6er, D. Haase, and J.-P. Katoen: Error Localization, Certificates, and Hints for Probabilistic Program Verification via Slicing (Artifact Evaluation), (2026). https:\/\/doi.org\/10.5281\/zenodo.18301089","DOI":"10.1007\/978-3-032-22723-2_8"},{"key":"8_CR51","unstructured":"P. Schr\u00f6er, D. Haase, and J.-P. Katoen: Error Localization, Certificates, and Hints for Probabilistic Program Verification via Slicing (Extended Version), (2025). arXiv: 2512.20214 [cs.PL]. https:\/\/arxiv.org\/abs\/2512.20214"},{"key":"8_CR52","doi-asserted-by":"publisher","unstructured":"M. Torres-Ruiz, R. Piedeleu, A. Silva, and F. Zanasi: On Iteration in Discrete Probabilistic Programming. In: J. Rehof. 9th International Conference on Formal Structures for Computation and Deduction, FSCD 2024, July 10-13, 2024, Tallinn, Estonia. LIPIcs, 20:1\u201320:21. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2024). https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2024.20","DOI":"10.4230\/LIPIcs.FSCD.2024.20"},{"key":"8_CR53","unstructured":"D. Tran, M.D. Hoffman, D. Moore, C. Suter, S. Vasudevan, and A. Radul: Simple, Distributed, and Accelerated Probabilistic Programming. In: S. Bengio, H.M. Wallach, H. Larochelle, K. Grauman, N. Cesa-Bianchi, and R. Garnett. Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018, NeurIPS 2018, December 3-8, 2018, Montr\u00e9al, Canada, pp. 7609\u20137620 (2018)"},{"key":"8_CR54","doi-asserted-by":"publisher","unstructured":"J.S. Vitter: Random Sampling with a Reservoir. ACM Trans. Math. Softw. 11(1), 37\u201357 (1985). https:\/\/doi.org\/10.1145\/3147.3165","DOI":"10.1145\/3147.3165"},{"key":"8_CR55","doi-asserted-by":"publisher","unstructured":"M.P. Ward and H. Zedan: Slicing as a program transformation. ACM Trans. Program. Lang. Syst. 29(2), 7 (2007). https:\/\/doi.org\/10.1145\/1216374.1216375","DOI":"10.1145\/1216374.1216375"},{"key":"8_CR56","doi-asserted-by":"publisher","unstructured":"M.D. Weiser: Program Slicing. IEEE Trans. Software Eng. 10(4), 352\u2013357 (1984). https:\/\/doi.org\/10.1109\/TSE.1984.5010248","DOI":"10.1109\/TSE.1984.5010248"},{"key":"8_CR57","doi-asserted-by":"publisher","unstructured":"R. Wimmer, N. Jansen, A. Vorpahl, E. \u00c1brah\u00e1m, J. Katoen, and B. Becker: High-level Counterexamples for Probabilistic Automata. Log. Methods Comput. Sci. 11(1) (2015). https:\/\/doi.org\/10.2168\/LMCS-11(1:15)2015","DOI":"10.2168\/LMCS-11(1:15)2015"},{"key":"8_CR58","doi-asserted-by":"publisher","unstructured":"B. Xu, J. Qian, X. Zhang, Z. Wu, and L. Chen: A brief survey of program slicing. ACM SIGSOFT Softw. Eng. Notes 30(2), 1\u201336 (2005). https:\/\/doi.org\/10.1145\/1050849.1050865","DOI":"10.1145\/1050849.1050865"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-22723-2_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,22]],"date-time":"2026-06-22T19:51:59Z","timestamp":1782157919000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-22723-2_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032227225","9783032227232"],"references-count":58,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-22723-2_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"10 April 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ESOP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"European Symposium on Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Turin","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 April 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"35","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/about\/esop\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}