Scalable Probabilistic Program Verification via Typed Extended Decision Diagrams: Artifact

Zenodo (CERN European Organization for Nuclear Research)

Abstract

This artifact accompanies the paper “Scalable Probabilistic Program Verification via Typed Extended Decision Diagrams”.It consists of a Docker image (ddsolve-popl.tar.gz) containing all required dependencies for the verification tools under test viz. caesar [1], storm [2], and our novel tool ddsolve [3]. The purpose of this artifact is to: 1. Reproduce the benchmark results reported in the paper including the figures used.2. Enable future users to analyse PGCL programs using ddsolve. All experiments can be executed on a standard x86_64/amd64 machine while only requiring a working Linux and Docker installation. The artifact is distributed as a Docker image archived in a gzip compressed tarball.The Docker image includes:1. Our tool ddsolve2. The probabilistic program verification tool caesar [1]3. The probabilistic model checker storm [2]4. All benchmark programs used in the paper5. The logs of the benchmark runs used for the figures in the paper. A virtualbox virtual machine image (ddsolve-vm.ova) is also provided but due to the resource intensive nature of the benchmark using it is not recommended.

Authors 4

1. Daniel Basgöze Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University

2. Kevin Batz Aachen

   RWTH Aachen University · University College London

   Affiliation as printed

   RWTH Aachen University

   University College London

3. Sebastian Junges

   Radboud University Nijmegen

   Affiliation as printed

   Radboud University

4. Joost-Pieter Katoen Aachen

   RWTH Aachen University · University of Twente

   Affiliation as printed

   RWTH Aachen University

   University of Twente