website: add arxiv link for slicing paper

Author: Philipp15b

website/blog/2025-12-23-esop26-slicing.md

@@ -4,7 +4,7 @@ authors: phisch
 tags: [publications]
 ---
 
-Our paper _"Error Localization, Certificates, and Hints for Probabilistic Program Verification via Slicing"_ was accepted at the [European Symposium on Programming (ESOP) 2026](https://etaps.org/2026/conferences/esop/) to be held in Turin, Italy.
+Our paper [_"Error Localization, Certificates, and Hints for Probabilistic Program Verification via Slicing"_](https://arxiv.org/abs/2512.20214) was accepted at the [European Symposium on Programming (ESOP) 2026](https://etaps.org/2026/conferences/esop/) to be held in Turin, Italy.
 The authors are Philipp Schröer, Darion Haase, and Joost-Pieter Katoen.
 
 The paper presents theoretical foundations and the implementation of our slicing-based user diagnostics in Caesar, which we dub *Brutus*.
@@ -13,6 +13,10 @@ See also the [announcement of Caesar 2.0](./2024-05-20-caesar-2-0.md), which int
 
 <!-- truncate -->
 
+<a href={require("/img/slicing-demo.png").default}>
+    <img src={require("/img/slicing-demo.png").default} style={{"float": "right", "maxWidth": "350px", "marginLeft": "1em"}} className="item shadow--tl" />
+</a>
+
 The theory is about *slices*, i.e. smaller sub-programs, to provide
  1. error localization (*error-witnessing slices*),
  2. proof simplification (*verification-witnessing slices*), and
@@ -22,6 +26,10 @@ These notions are defined on the quantitative intermediate verification language
 Based on these notions, specialized slicing-based diagnostics are provided for various proof rules, such as the [induction proof rule](/docs/proof-rules/induction) or [procedure calls](/docs/heyvl/procs) (called *specification statements* in the paper).
 The correctness of the above is formally proven in the paper.
 
+<a href={require("/img/general-slicing-demo.png").default}>
+    <img src={require("/img/general-slicing-demo.png").default} style={{"float": "right", "maxWidth": "400px", "marginLeft": "1em"}} className="item shadow--tl" />
+</a>
+
 The paper also reports on the implementation of these ideas.
 We explain the algorithms to compute the different slice types efficiently.
 For error reporting, we use a binary search-based algorithm to find minimal error-witnessing slices.

website/docs/publications.md

@@ -29,7 +29,10 @@ import TOCInline from '@theme/TOCInline';
 
 ### ESOP '26: Error Localization, Certificates, and Hints for Probabilistic Program Verification via Slicing
 
-The paper _"Error Localization, Certificates, and Hints for Probabilistic Program Verification via Slicing"_ by Philipp Schröer, Darion Haase, and Joost-Pieter Katoen was accepted at the [European Symposium on Programming (ESOP) 2026](https://etaps.org/2026/conferences/esop/) to be held in Turin, Italy.
+The paper [_"Error Localization, Certificates, and Hints for Probabilistic Program Verification via Slicing"_](https://arxiv.org/abs/2512.20214) by Philipp Schröer, Darion Haase, and Joost-Pieter Katoen was accepted at the [European Symposium on Programming (ESOP) 2026](https://etaps.org/2026/conferences/esop/) to be held in Turin, Italy.
+
+An **extended version with proofs and additional material** is available on arXiv: [Error Localization, Certificates, and Hints for Probabilistic Program Verification via Slicing (Extended Version) — arXiv:2512.20214](https://arxiv.org/abs/2512.20214).
+
 The paper presents theoretical foundations and the implementation of our slicing-based user diagnostics in Caesar, dubbed *Brutus*, and introduces different kinds of slices: error-witnessing (for error localization), verification-witnessing (for proof simplification), and verification-preserving (to maintain successful verification results).
 
 Further links:
@@ -70,7 +73,7 @@ For publication, please cite as follows ([BibTeX file](https://dblp.org/rec/jour
 
 > Philipp Schröer, Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja. *A Deductive Verification Infrastructure for Probabilistic Programs.* Proceedings of the ACM on Programming Languages 7, OOPSLA 2023. DOI: https://doi.org/10.1145/3622870.
 
-An **extended version with proofs, details on encodings, and typo fixes** is available on arXiv: [A Deductive Verification Infrastructure for Probabilistic Programs (extended version) — arXiv:2309.07781](https://arxiv.org/abs/2309.07781).
+An **extended version with proofs, details on encodings, and typo fixes** is available on arXiv: [A Deductive Verification Infrastructure for Probabilistic Programs (Extended Version) — arXiv:2309.07781](https://arxiv.org/abs/2309.07781).
 
 **The artifact** for our OOPSLA '23 publication is [available on Zenodo](https://zenodo.org/record/8146987).
 [It has received the *Distinguished Artifact* award](/blog/2023/10/27/oopsla23-distinguished-artifact), praising exceptionally high quality of the artifact.