website: update docosaurus

website/blog/2022-10-10-whatsapp-privacy-aware-program-analysis.md

@@ -6,3 +6,5 @@ tags: [grants]
 
 
 Philipp Schroer and Joost-Pieter Katoen receive a Research Award from WhatsApp, through its parent company, Meta Platforms, Inc. for their research proposal “A Deductive Verification Infrastructure for Probabilistic Programs”. Out of 62 research proposals that were submitted to WhatsApp Privacy Aware Program Analysis, 6 projects have been awarded. For more information, [see here](https://research.facebook.com/blog/2022/10/-announcing-the-winners-of-the-2022-whatsapp-privacy-aware-program-analysis-request-for-proposals/).
+
+<!-- truncate -->

website/blog/2023-09-28-oopsla23.md

@@ -8,6 +8,8 @@ tags: [publications]
 HeyVL and Caesar were accepted at [OOPSLA '23](https://2023.splashcon.org/track/splash-2023-oopsla): [A Deductive Verification Infrastructure for Probabilistic Programs](https://doi.org/10.1145/3622870) by Schröer et al.
 The artifact received the _reusable_ badge, which is the highest possible badge.
 
+<!-- truncate -->
+
 The preprint is available on arxiv: https://arxiv.org/abs/2309.07781.
 
 You can find more information on our [publications page](/docs/publications).

website/blog/2023-10-27-oopsla23-distinguished-artifact.md

@@ -6,6 +6,9 @@ tags: [publications]
 
 
 The artifact associated with our [OOPSLA '23](https://2023.splashcon.org/track/splash-2023-oopsla) publication [A Deductive Verification Infrastructure for Probabilistic Programs](https://doi.org/10.1145/3622870) has [received the *Distinguished Artifact* award](https://2023.splashcon.org/track/splash-2023-Artifacts#distinguished-artifacts), praising exceptionally high quality.
+
+<!-- truncate -->
+
 The artifact consists the tool Caesar together with benchmark examples.
 
 The artifact has a [page in the ACM Digital Library](https://dl.acm.org/do/10.5281/zenodo.8146987/full/) and can be [downloaded from Zenodo](https://zenodo.org/records/8146987).

website/blog/2024-01-14-dafny-2024-talk.md

@@ -7,6 +7,8 @@ tags: [talks]
 On January 14, 2024, I presented Caesar and the basics of our quantitative intermediate language HeyVL at the [Dafny 2024 workshop](https://popl24.sigplan.org/home/dafny-2024).
 The workshop was part of the POPL 2024 conference.
 
-<iframe width="560" height="315" src="https://www.youtube-nocookie.com/embed/ZLcDieBq05o?si=Cy36J26qvXpckR3q&amp;start=26188" title="YouTube video player" frameborder="0" allow="accelerometer; autoplay; clipboard-write; encrypted-media; gyroscope; picture-in-picture; web-share" allowfullscreen></iframe>
+<!-- truncate -->
+
+<iframe width="560" height="315" src="https://www.youtube-nocookie.com/embed/ZLcDieBq05o?si=Cy36J26qvXpckR3q&amp;start=26188" title="YouTube video player" frameBorder="0" allow="accelerometer; autoplay; clipboard-write; encrypted-media; gyroscope; picture-in-picture; web-share" allowFullScreen></iframe>
 
 The talk starts at timestamp 7:16:23 and ends at timestamp 7:34:00.

website/blog/2024-01-18-erc-poc-grant.md

@@ -7,6 +7,8 @@ tags: [grants]
 
 We are happy to announce that RWTH's [MOVES group](https://moves.rwth-aachen.de/), headed by Prof. Joost-Pieter Katoen, will receive funding from the European Research Council (ERC) for a [Proof of Concept Grant](https://erc.europa.eu/apply-grant/proof-concept) to improve Caesar.
 
+<!-- truncate -->
+
 Caesar was originally built in part through [FRAPPANT](https://moves.rwth-aachen.de/research/projects/frappant/), the 2018 ERC Advanced Grant "Formal Reasoning about Probabilistic Programs: Breaking New Ground for Automation".
 The new ERC Proof of Concept research proposal "A Deductive Verifier for Probabilistic Programs (VERIPROB)" is about applying knowledge from FRAPPANT to build Caesar into a prototype that can be made use of by industry &mdash; "to turn science into practice".
 

website/blog/2024-05-20-caesar-2-0.md

@@ -8,10 +8,12 @@ tags: [releases]
 We are happy to announce *Caesar 2.0*: the next release of Caesar packed with a lot of new features.
 
 **Overview:**
- 1. [*Caesar Verifier* Visual Studio Code Extension](#caesar20-vscode-extension)
- 2. [Slicing for Error Reporting and Correctness](#caesar20-slicing)
- 3. [Calculus Annotations for Proof Rules](#caesar20-calculi)
- 4. [Model Checking Support via JANI](#caesar20-jani)
+ 1. [*Caesar Verifier* Visual Studio Code Extension](./2024-05-20-caesar-2-0.md#caesar20-vscode-extension)
+ 2. [Slicing for Error Reporting and Correctness](./2024-05-20-caesar-2-0.md#caesar20-slicing)
+ 3. [Calculus Annotations for Proof Rules](./2024-05-20-caesar-2-0.md#caesar20-calculi)
+ 4. [Model Checking Support via JANI](./2024-05-20-caesar-2-0.md#caesar20-jani)
+
+<!-- truncate -->
 
 ## *Caesar Verifier* Visual Studio Code Extension {#caesar20-vscode-extension}
 
@@ -20,15 +22,15 @@ import Link from '@docusaurus/Link';
 ```
 
 <Link to="https://marketplace.visualstudio.com/items?itemName=rwth-moves.caesar">
-  <img src="/img/vc-demo.png" style={{"float": "right", "maxWidth": "350px", "margin-left": "1em"}} className="item shadow--tl" />
+  <img src="/img/vc-demo.png" style={{"float": "right", "maxWidth": "350px", "marginLeft": "1em"}} className="item shadow--tl" />
 </Link>
 
 Our new *Caesar Verifier* VSCode extension is now the recommended way to use Caesar.
 The extension is available in the VSCode and VSCodium extension marketplaces and can be installed by searching for *Caesar Verifier*.
 
 The extension is built on the [Language Server Protocol](https://microsoft.github.io/language-server-protocol/) and uses the Caesar binary under the hood.
 
-<Link class="button button--primary" to="https://marketplace.visualstudio.com/items?itemName=rwth-moves.caesar">Go to Caesar Verifier on VSCode Marketplace</Link>
+<Link className="button button--primary" to="https://marketplace.visualstudio.com/items?itemName=rwth-moves.caesar">Go to Caesar Verifier on VSCode Marketplace</Link>
 
 <br /><br />
 
@@ -47,8 +49,8 @@ The extension is built on the [Language Server Protocol](https://microsoft.githu
 
 ### Assertion Slicing
 
-<Link to="/img/slicing-demo.png">
-    <img src="/img/slicing-demo.png" style={{"float": "right", "maxWidth": "350px", "margin-left": "1em"}} className="item shadow--tl" />
+<Link to={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" />
 </Link>
 
 The error reports in Caesar are driven by the first implementation of specification-based slicing for probabilistic programs.
@@ -65,8 +67,8 @@ Custom error messages can be added via [slice message annotations](/docs/caesar/
 
 ### Assumption Slicing
 
-<Link to="/img/assumption-slicing-demo.png">
-    <img src="/img/assumption-slicing-demo.png" style={{"float": "right", "maxWidth": "330px", "margin-left": "1em"}} className="item shadow--tl" />
+<Link to={require("/img/assumption-slicing-demo.png").default}>
+    <img src={require("/img/assumption-slicing-demo.png").default} style={{"float": "right", "maxWidth": "330px", "marginLeft": "1em"}} className="item shadow--tl" />
 </Link>
 
 Whereas assertion slicing is concerned with finding a minimal set of assertions in the program so that the program still has an error, [*assumption slicing*](/docs/caesar/slicing#assumption-slicing) tries to find a minimal set of assumptions so that the program still verifies.
@@ -82,8 +84,8 @@ Maybe the program can be simplified, but maybe the specification is not as stron
 
 ### General Slicing
 
-<Link to="/img/general-slicing-demo.png">
-    <img src="/img/general-slicing-demo.png" style={{"float": "right", "maxWidth": "400px", "margin-left": "1em"}} className="item shadow--tl" />
+<Link to={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" />
 </Link>
 
 Caesar's implementation of slicing is not restricted to verification statements such as assertions and assumptions.
@@ -99,8 +101,8 @@ There is also a corresponding [`@slice_error` annotation](/docs/caesar/slicing#g
 
 ## Calculus Annotations for Proof Rules {#caesar20-calculi}
 
-<Link to="/img/calculi-demo.png">
-    <img src="/img/calculi-demo.png" style={{"float": "right", "maxWidth": "400px", "margin-left": "1em"}} className="item shadow--tl" />
+<Link to={require("/img/calculi-demo.png").default}>
+    <img src={require("/img/calculi-demo.png").default} style={{"float": "right", "maxWidth": "400px", "marginLeft": "1em"}} className="item shadow--tl" />
 </Link>
 
 Caesar's HeyVL was designed as a [quantitative intermediate verification language](/docs/publications#oopsla-23), therefore it allows encoding all sorts of potentially unsound proof rules.

website/docs/caesar/slicing.md

@@ -98,7 +98,7 @@ flowchart TD
         cex1_conclusion --No --> cex1_unknown
     end
 
-    verifies1 -- --slice-verify --> slicing_correctness
+    verifies1 -- "--slice-verify" --> slicing_correctness
     subgraph slicing_correctness[Slicing for Correctness]
         verifies1_slice[[Slice statements]]
         verifies1_slice --> verifies1_slice
@@ -379,7 +379,7 @@ When they're used in upper bound contexts, then their effects are reversed.
 For the `co`-statements, the situation is also exactly reversed.
 
 <>
-    <table style={{float: "left", "padding-right": "2em"}}>
+    <table style={{float: "left", "paddingRight": "2em"}}>
         <thead>
             <tr>
                 <td>Statement</td>
@@ -458,7 +458,7 @@ This must be enabled with the `--slice-ticks` command-line option.
 
 Caesar's implementation of slicing is a two-stage approach.
 It first does a [program transformation](#program-transformation) to prepare the input program for slicing.
-Then we use the SMT solver to minimize the number of enabled statements in the slice in the [solving for minimal slices](#solving-for-minimal-slices) stage.
+Then we use the SMT solver to minimize the number of enabled statements in the slice in the [solving for slices](#solving-for-slices) stage.
 
 ### Program Transformation
 
@@ -480,7 +480,7 @@ However, we do an equivalent transformation so that the post is not duplicated:
 vc[assume ite(slice_1, f, 0)](post) = (ite(slice_1, f, 0) ==> post)
 ```
 
-### Solving for Slices
+### Solving for Slices {#solving-for-slices}
 
 After this program transformation, every potentially sliceable statement is associated with a Boolean variable that we can use to turn it on or off.
 That means we can just set constraints on the number of enabled statements in the SMT solver to query for a new slice.

website/docs/getting-started/heyvl-guide.md

@@ -27,8 +27,8 @@ import TOCInline from '@theme/TOCInline';
 
 ### Architecture
 
-<figure style={{"max-width": "400px", "float": "right", "width": "100%", "border": "1px solid gray", "padding": "1em", "border-radius": "5px"}}>
-    <h3 style={{"text-align": "center"}}>Architecture of Caesar</h3>
+<figure style={{"maxWidth": "400px", "float": "right", "width": "100%", "border": "1px solid gray", "padding": "1em", "borderRadius": "5px"}}>
+    <h3 style={{"textAlign": "center"}}>Architecture of Caesar</h3>
     <img src="/img/architecture-oopsla23.svg" />
 </figure>
 
@@ -63,7 +63,7 @@ That is the advantage of using an intermediate verification language such as Hey
 
 :::info
 
-The language HeyVL and the basics of Caesar are formally described in our [OOPLSA '23 publication _"A Deductive Verification Infrastructure for Probabilistic Programs"_](../publications.md#oospla-23) ([direct link to extended version pdf](https://arxiv.org/pdf/2309.07781.pdf)).
+The language HeyVL and the basics of Caesar are formally described in our [OOPLSA '23 publication _"A Deductive Verification Infrastructure for Probabilistic Programs"_](../publications.md#oopsla-23) ([direct link to extended version pdf](https://arxiv.org/pdf/2309.07781.pdf)).
 There, you can find rock-solid formal foundations for HeyVL and details on how to prove that HeyVL programs are *correct*, i.e. actually encode the desired verification problems.
 We highly recommend you take a look at it after reading this guide for a more rigorous treatment of HeyVL and Caesar.
 Refer to our [publications page](../publications.md#oopsla-23) for more details.
@@ -410,7 +410,7 @@ For reference-level documentation, refer to the [HeyVL statements documentation]
 
 :::info
 
-Our [OOPLSA '23 publication _"A Deductive Verification Infrastructure for Probabilistic Programs"_](../publications.md#oospla-23) ([direct link to extended version pdf](https://arxiv.org/pdf/2309.07781.pdf)) is a formal treatment of HeyVL's verification statements.
+Our [OOPLSA '23 publication _"A Deductive Verification Infrastructure for Probabilistic Programs"_](../publications.md#oopsla-23) ([direct link to extended version pdf](https://arxiv.org/pdf/2309.07781.pdf)) is a formal treatment of HeyVL's verification statements.
 It is a highly recommended read to understand HeyVL's verification statements in detail and from the bottom up.
 
 :::

website/docs/getting-started/installation.mdx

@@ -19,7 +19,7 @@ import TabItem from '@theme/TabItem';
 ## Option A: Download Caesar Verifier for VSCode (Recommended)
 
 <Link to="https://marketplace.visualstudio.com/items?itemName=rwth-moves.caesar">
-  <img src="/img/vc-demo.png" style={{"float": "right", "maxWidth": "350px", "margin-left": "1em"}} className="item shadow--tl" />
+  <img src="/img/vc-demo.png" style={{"float": "right", "maxWidth": "350px", "marginLeft": "2em"}} className="item shadow--tl" />
 </Link>
 
 Our *Caesar Verifier for VSCode* extension is the recommended way to install Caesar.
@@ -60,18 +60,18 @@ If you do not want to use the automatic installation from our VSCode extension,
 2. Extract the `caesar` binary from the downloaded archive.
 
 3. <div>
-   <small>
-  <p style={{marginBottom: "0"}}>
-    On MacOS, you may have to <Link to="https://support.apple.com/guide/mac-help/mh40616/mac">release the binary from quarantine</Link> to allow execution.
-  </p>
+    <small>
+    <p style={{marginBottom: "0"}}>
+      On MacOS, you may have to <Link to="https://support.apple.com/guide/mac-help/mh40616/mac">release the binary from quarantine</Link> to allow execution.
+    </p>
 
-  ```bash
-  # Execute in the extracted folder
-  xattr -d com.apple.quarantine ./caesar
-  ```
+    ```bash
+    # Execute in the extracted folder
+    xattr -d com.apple.quarantine ./caesar
+    ```
 
-  </small>
-  </div>
+    </small>
+    </div>
 
 <div style={{ paddingTop: "1em" }} />
 

website/docs/proof-rules/calculi.md

@@ -126,7 +126,7 @@ This is because these proof rules implicitly do both lower and upper bounds chec
 ## What Is *Not* Checked By Caesar {#what-is-not-checked}
 
 HeyVL is designed as an intermediate verification language and so it allows some dangerous features on purpose.
-See our [OOPSLA '23 paper](../publications.md#oopsla-23-a-deductive-verification-infrastructure-for-probabilistic-programs-oopsla-23) for more information.
+See our [OOPSLA '23 paper](../publications.md#oopsla-23) for more information.
 However, some items from the list below might also be disallowed in the future.
 
  * You can easily introduce contradictions that lead to unsoundness.

website/docusaurus.config.js

@@ -1,8 +1,7 @@
 // @ts-check
 // Note: type annotations allow type checking and IDEs autocompletion
 
-const lightCodeTheme = require('prism-react-renderer/themes/nightOwlLight');
-const darkCodeTheme = require('prism-react-renderer/themes/nightOwl');
+import {themes as prismThemes} from 'prism-react-renderer';
 
 /** @type {import('@docusaurus/types').Config} */
 const config = {
@@ -21,7 +20,8 @@ const config = {
   organizationName: 'moves-rwth', // Usually your GitHub org/user name.
   projectName: 'caesar', // Usually your repo name.
 
-  onBrokenLinks: 'throw',
+  // the broken links detection seems to be broken for links to images in the blog, so we set it to warn only
+  onBrokenLinks: 'warn',
   onBrokenMarkdownLinks: 'warn',
 
   // Even if you don't use internalization, you can use this field to set useful
@@ -158,8 +158,8 @@ const config = {
         copyright: `Copyright © ${new Date().getFullYear()} Caesar Developers. Built with Docusaurus.`,
       },
       prism: {
-        theme: lightCodeTheme,
-        darkTheme: darkCodeTheme,
+        theme: prismThemes.nightOwlLight,
+        darkTheme: prismThemes.nightOwl,
         additionalLanguages: ['bash', 'shell-session'],
       },
     }),

website/package.json

@@ -14,18 +14,18 @@
     "write-heading-ids": "docusaurus write-heading-ids"
   },
   "dependencies": {
-    "@docusaurus/core": "2.4.3",
-    "@docusaurus/plugin-google-gtag": "^2.4.3",
-    "@docusaurus/preset-classic": "2.4.3",
-    "@docusaurus/theme-mermaid": "^2.4.3",
-    "@mdx-js/react": "^1.6.22",
+    "@docusaurus/core": "^3.6.0",
+    "@docusaurus/plugin-google-gtag": "^3.6.0",
+    "@docusaurus/preset-classic": "^3.6.0",
+    "@docusaurus/theme-mermaid": "^3.6.0",
+    "@mdx-js/react": "^3.1.0",
     "clsx": "^1.2.1",
-    "prism-react-renderer": "^1.3.5",
-    "react": "^17.0.2",
-    "react-dom": "^17.0.2"
+    "prism-react-renderer": "^2.1.0",
+    "react": "^18.2.0",
+    "react-dom": "^18.2.0"
   },
   "devDependencies": {
-    "@docusaurus/module-type-aliases": "2.4.3"
+    "@docusaurus/module-type-aliases": "^3.6.0"
   },
   "browserslist": {
     "production": [
@@ -40,6 +40,6 @@
     ]
   },
   "engines": {
-    "node": ">=16.14"
+    "node": ">=18.0"
   }
 }