Our paper “Fast Debugging of PRISM Models” by Christian Dehnert, Nils Jansen, Ralf Wimmer, Erika Ábrahám and Joost-Pieter Katoen was accepted at ATVA 2014. The paper presents a new way to compute critical parts of a PRISM program by utilizing a MAX-SAT solver. This is the first approach rendering the computation of these sort of […]

The paper “Parametric LTL on Markov Chains” by Souymodip Chakraborty and Joost-Pieter Katoen has been accepted at the IFIP TCS conference. The paper shows the undecidability of verifying a Markov chain against a parametric LTL (pLTL) formula, and studies the complexity of model checking several logical fragments of pLTL.

The paper “Tight Game Abstractions of Probabilistic Automata” by Falak Sher and Joost-Pieter Katoen has been accepted at the conference Concurrency Theory. The paper presents game-based abstraction that is based on abstracting distributions (rather than states) and shows that this yields more accurate abstraction than state-based abstractions.

The paper “Minimal Counterexamples for Linear-Time Probabilistic Verification” by Ralf Wimmer, Nils Jansen, Erika Ábrahám, Joost-Pieter Katoen and Bernd Becker was accepted for publication in the journal Theoretical Computer Science. The paper thoroughly examines the possibilities for computing so-called minimal critical subsystems for Markov decision processes by means of mixed integer linear programming.

A survey paper concerning the generation of counterexamples for probabilistic systems was published by Erika Ábrahám, Bernd Becker, Christian Dehnert, Nils Jansen, Joost-Pieter Katoen and Ralf Wimmer within the scope of the PhD school SFM in Bertinoro, Italy. This paper gives a nice introduction to the foundations and the state-of-the-art of this topic, explaining all methods […]

The paper “Accelerating Parametric Probabilistic Verification” by Nils Jansen, Florian Corzilius, Matthias Volk, Ralf Wimmer, Erika Ábrahám, Joost-Pieter Katoen and Bernd Becker was accepted at QEST 2014 in Florence. The paper considers a new approach on Model Checking parametric discrete-time Markov chains based on eliminating the strongly connected components of the system graph. Together with […]

The papers “Generating Inductive Predicates for Symbolic Execution of Pointer-Manipulating Programs” by Christina Jansen, Florian Göbe, and Thomas Noll, and “Generating Abstract Graph-Based Procedure Summaries for Pointer Programs” by Christina Jansen and Thomas Noll have been accepted at ICGT 2014 in York, GB.  The former paper relates two abstraction approaches for pointer programs, graph grammars and […]

The papers “Probably Safe or Live” by Katoen, Song and Zhang, and “Zero-Reachability in Probabilistic Multi-Counter Automata” by Brazdil, Kiefer, Kucera, Novotny and Katoen have been accepted at CSL-LICS 2014 in Vienna.  The former paper classifies safety and liveness properties in the probabilistic setting while the second paper sets the ground for showing some flaws […]

The paper entitled “Layered Reduction for Abstract Probabilistic Automata” by Arpit Sharma and Joost-Pieter Katoen has been accepted for  the 14th Int. Conf. on Application of Concurrency on System Design (ACSD) 2014.