Operational Versus Weakest Precondition Semantics for the Probabilistic Guarded Command Language. - Friedrich Gretz; Joost-Pieter Katoen; Annabelle McIver (QEST, 2012)

Prinsys - On a Quest for Probabilistic Loop Invariants. - Friedrich Gretz; Joost-Pieter Katoen; Annabelle McIver (QEST, 2013)

Invariant Generation for Probabilistic Programs. - Friedrich Gretz (Joint Workshop of the German Research Training Groups in Computer Science, 2014)

Operational versus weakest pre-expectation semantics for the probabilistic guarded command language. - Friedrich Gretz; Joost-Pieter Katoen; Annabelle McIver (Perform. Evaluation, 2014)

Understanding Probabilistic Programs. - Joost-Pieter Katoen; Friedrich Gretz; Nils Jansen 001; Benjamin Lucien Kaminski; Federico Olmedo (Correct System Design, 2015)

Conditioning in Probabilistic Programming. - Nils Jansen 001; Benjamin Lucien Kaminski; Joost-Pieter Katoen; Federico Olmedo; Friedrich Gretz; Annabelle McIver (MFPS, 2015)

Semantics and loop invariant synthesis for probabilistic programs. - Friedrich Gretz (2016)

Blech, Imperative Synchronous Programming! - Friedrich Gretz; Franz-Josef Grosch (FDL, 2018)

Synchronized Shared Memory and Procedural Abstraction: Towards a Formal Semantics of Blech. - Friedrich Gretz; Franz-Josef Grosch; Michael Mendler; Stephan Scheele (FDL, 2020)

Extracting Mode Diagrams from Blech Code. - Daniel Lucas; Alexander Schulz-Rosengarten; Reinhard von Hanxleden; Friedrich Gretz; Franz-Josef Grosch (FDL, 2021)

Synchronized Shared Memory and Black-box Procedural Abstraction: Toward a Formal Semantics of Blech. - Friedrich Gretz; Franz-Josef Grosch; Michael Mendler; Stephan Scheele (ACM Trans. Embed. Comput. Syst., 2024)