The paper “Quantitative Model Checking of Discrete-Time Markov Processes” by Ilya Tkachev, Alexandru Mereacre, Joost-Pieter Katoen, and Alessandro Abate has been accepted for publication in Information and Computation.  The almost 50-page paper focuses on optimizing (repeated) reachability probabilities of events of interest defined over general controlled discrete-time Markov processes.  Unlike known results over finite-state models, […]

Dino Distefano (FaceBook and Queen Mary University) received the CAV Award 2016, together with his co-workers, for their work on Separation Logic and demonstrating its applicability on the automated verification of dynamic data structures.  Dino is the first Ph.D. student of Joost-Pieter Katoen, who supervised him together with Arend Rensink (Twente).

The paper “Performance Evaluation on Modern Concurrent Data Structures” by Hao Wu, Xiaoxiao Yang and Joost-Pieter Katoen has been accepted at SETTA 2016 in Beijing.  The paper considers the modelling of several concurrent data structures in LOTOS-NT and evaluates their performance by model-based analysis.

Joost-Pieter Katoen will give an invited talk on “The Probabilistic Model Checking Landscape” at LICS 2016 in New York City, early July 2016.  The accompanying paper can be found here.

The paper “Inferring Covariances for Probabilistic Programs” by Benjamin Kaminski, Joost-Pieter Katoen and Christoph Matheja has been accepted at the Int. Conf. on Quantitative Evaluation of SysTems (QEST) in Quebec City, Canada.  The paper shows that approximating (co)variances is computationally more difficult than approximating expected values and presents invariant-based techniques for approximating both upper and […]

Two new papers have been accepted at SAFECOMP 2016 in Trondheim, Norway. The paper “Advancing Dynamic Fault Tree Analysis” by Matthias Volk, Sebastian Junges, and Joost-Pieter Katoen presents a mixture of a new state-space generation technique together with several reduction techniques for dynamic fault trees.  Experiments results show improvements of up to five orders of […]

The paper “Probabilistic Model Checking for Uncertain Scenario-Aware Data Flow” by Joost-Pieter Katoen and Hao Wu has been accepted for publication in the journal ACM Transactions on Embedded Computing Systems.  A short version thereof received the best paper award at the IDEA Workshop during the CPS week 2016. Based on a compositional semantics of exponentially-timed S(A)DF […]

The paper “Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs” by Benjamin Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Federico Olmedo, has received the EATCS Best Paper Award at ETAPS 2016.  Out of 473 submissions, this paper was selected as one of the two  best theory papers at ETAPS 2016.

The paper “Reasoning about Recursive Probabilistic Programs” by Federico Olmedo, Benjamin Lucien Kaminski, Joost-Pieter Katoen and Christoph Matheja, as well as the paper “On the Satisfiability of Some Simple Probabilistic Logics” by Souymodip Chakraborty and Joost-Pieter Katoen have been accepted at LICS 2016. The former paper presents a wp-calculus and accompanying proof rules for recursive […]

The paper “Uncovering Dynamic Fault Trees” by Sebastian Junges, Dennis Guck, Joost-Pieter Katoen and Marielle Stoelinga has been accepted for publication at DSN 2016.  The paper presents a thorough discussion of the semantic intricacies of dynamic fault trees and a comparison of existing interpretations of such fault trees.