The paper entitled “A Deductive Verification Infrastructure for Probabilistic Programs” by Philipp Schröer, Kevin Batz, Benjamin Kaminski (Saarland University and UCL), Joost-Pieter Katoen and Christoph Matheja (TU Denmark) has been accepted for publication at OOPSLA 2023. The paper presents a quantitative program verification infrastructure for discrete probabilistic programs. This infrastructure can be viewed as the probabilistic analogue of Boogie: its central components are an intermediate verification language (IVL) together with a real-valued logic.

The associated tool Caesar is available on its website www.caesarverifier.org.