website: add new publication by Christoph!

website/blog/2024-12-31-game-based-semantics.md

@@ -0,0 +1,22 @@
+---
+authors: phisch
+tags: [publications]
+---
+
+# A Game-Based Operational Semantics for HeyVL
+
+The publication [_"A Game-Based Semantics for the Probabilistic
+Intermediate Verification Language HeyVL"_](https://doi.org/10.1007/978-3-031-75434-0_17) by Christoph Matheja was published at [AISoLA 2024](https://2024-isola.isola-conference.org/) and is now available online.
+
+<!-- truncate -->
+
+Quoting from its abstract:
+
+> [T]he original language [HeyVL] lacked a formal “ground truth” in terms of a small-step operational semantics that enables an intuitive reading of HeyVL programs.
+>
+> In this paper, we define an operational semantics for a cleaned-up version of HeyVL in terms of *refereed* stochastic games, a novel extension of simple stochastic games in which a referee may perform quantitative reasoning about the expected outcome of sub-games and give one player an advantage if those sub-game are outside of certain boundaries.
+
+This new operational semantics is aimed at improved intuition and ergonomics of HeyVL, as well as a possible future work enabling other verification backends such as ones based on probabilistic model checking tools.
+
+Note that the existing [model checking backend](/docs/model-checking) of Caesar does not yet support for the full extent of the HeyVL language, but merely an "executable subset".
+Therefore, this publication shows an avenue for a future extension of this existing backend via refereed stochastic games.

website/docs/publications.md

@@ -9,11 +9,24 @@ Caesar is a project from a collaboration of the [Chair for Software Modeling and
 
 If you are interested in collaborations or simply have some questions, please reach out to [Philipp Schroer](https://moves.rwth-aachen.de/people/philipp-schroer/) ([[email protected]](mailto:[email protected])).
 
+## AISoLA '24: A Game-Based Semantics for the Probabilistic Intermediate Verification Language HeyVL
+
+The publication [_"A Game-Based Semantics for the Probabilistic
+Intermediate Verification Language HeyVL"_](https://doi.org/10.1007/978-3-031-75434-0_17) by Christoph Matheja was published at [AISoLA 2024](https://2024-isola.isola-conference.org/). DOI: https://doi.org/10.1007/978-3-031-75434-0_17.
+
+Quoting from its abstract:
+
+> [T]he original language [HeyVL] lacked a formal “ground truth” in terms of a small-step operational semantics that enables an intuitive reading of HeyVL programs.
+>
+> In this paper, we define an operational semantics for a cleaned-up version of HeyVL in terms of *refereed* stochastic games, a novel extension of simple stochastic games in which a referee may perform quantitative reasoning about the expected outcome of sub-games and give one player an advantage if those sub-game are outside of certain boundaries.
+
+This new operational semantics is aimed at improved intuition and ergonomics of HeyVL, as well as a possible future work enabling other verification backends such as ones based on probabilistic model checking tools.
+
 ## OOPSLA '23: A Deductive Verification Infrastructure for Probabilistic Programs {#oopsla-23}
 
 HeyVL and Caesar were first published 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.
 
-For publication, please cite as follows: 
+For publication, please cite as follows:
 
 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.
 

website/docusaurus.config.js

@@ -50,9 +50,8 @@ const config = {
             'https://github.com/moves-rwth/caesar/tree/main/website/',
         },
         blog: {
+          blogSidebarCount: 20,
           showReadingTime: true,
-          // Please change this to your repo.
-          // Remove this to remove the "edit this page" links.
           editUrl:
             'https://github.com/moves-rwth/caesar/tree/main/website/',
         },