Two new papers have been accepted at ATVA 2016 in Chiba, Japan.

The paper “Bounded Model Checking for Probabilistic Program” by Nils Jansen, Christian Dehnert, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Lukas Westhofen describes an automated on-the-fly verification approach for probabilistic programs. It incorporates key features such as conditioning and parametric probabilities. Experiments show the feasibility and scalability on a wide range of benchmarks.

The paper “Parameter Synthesis for Markov Models: Faster Than Ever” by Tim Quatmann, Christian Dehnert, Nils Jansen, Sebastian Junges and Joost-Pieter Katoen presents a parameter space partitioning algorithm for parametric DTMCs, via a reduction to MDPs. The beauty of the approach is that it naturally extends to parametric MDPs, which can be solved via stochastic games. The new algorithm is experimentally shown to be orders of magnitude faster than existing approaches.