Caesar: A Deductive Verifier for Probabilistic Programs

Lecture notes in computer science, pp. 565–582

Abstract

Abstract is a deductive verifier for probabilistic programs. At its core lies , a quantitative intermediate verification language based on the real-valued logic . allows users to express a probabilistic program, its specifications, and proof rules in a programming-language style, so that new proof rules can be easily integrated into the verifier. translates programs into verification conditions, which are then checked using the Z3 SMT solver. It also includes a backend based on probabilistic model checking for a subset of . We report on the results of five years of development of , highlighting its main features and architecture. In particular, we describe recent improvements such as additional proof rules, a model-checking backend, and better diagnostics.

Authors 7

1. Philipp Schröer corresponding Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University, Aachen, Germany

2. Kevin Batz

   Cornell University

   Affiliation as printed

   Cornell University, New York City, USA

3. Umut Yiğit Dural Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University, Aachen, Germany

4. Darion Haase Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University, Aachen, Germany

5. Benjamin Lucien Kaminski

   University College London · Saarland University

   Affiliation as printed

   Saarland University, Saarbrücken, Germany

   University College London, London, UK

6. Joost-Pieter Katoen Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University, Aachen, Germany

7. Christoph Matheja

   Carl von Ossietzky Universität Oldenburg · Technical University of Denmark

   Affiliation as printed

   DTU Compute, Lundtofte, Denmark

   University of Oldenburg, Oldenburg, Germany