News

LICS’17 paper accepted

March 22, 2017

The paper “A Weakest Pre-Expectation Semantics for Mixed-Sign Expectations” by Benjamin L. Kaminski and Joost-Pieter Katoen has been accepted to LICS 2017\. The paper presents a wp–style calculus for

Probabilistic Model Checker Storm: First Release

January 29, 2017

We launch the new probabilistic model checker Storm. It features the analysis of discrete- and continuous-time variants of both Markov chains and MDPs. It supports the Prism and JANI modeling language

Workshop on Learning in Verification (LiVe)

January 9, 2017

At ETAPS 2017, a workshop on Learning in Verification takes place. The aim of the workshop is to stimulate discussion on the potential of learning techniques in verification and to report on recent ad

Two papers accepted at TACAS 2017

December 22, 2016

The paper “Sequential Convex Programming for the Efficient Verification of Parametric MDPs” by Murat Cubuktepe, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen, Ivan Papusha, Hasan A. Poonawala,

Paper accepted at ESOP 2017

December 17, 2016

The paper “Unified Reasoning about Robustness Properties of Symbolic-Heap Separation Logic” by Christina Jansen, Jens Katelaan, Christoph Matheja, Thomas Noll and Florian Zuleger has been accepted at

Paper accepted in Formal Aspects of Computing

November 22, 2016

The paper “Fault Trees on a Diet: Automated Reduction by Graph Rewriting” by Sebastian Junges, Dennis Guck, Arend Rensink, Marielle Stoelinga and Joost-Pieter Katoen has been accepted in the journal F

Paper accepted in Information & Computation

August 30, 2016

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 Informatio

CAV Award 2016

August 6, 2016

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 v

Paper accepted at SETTA’16

August 6, 2016

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 o

AADL Standards Meeting

July 15, 2016

From July 25 to 28, our group hosts the Summer meeting of the [AADL Standardization Committee](https://wiki.sei.cmu.edu/aadl/index.php/Standardization). The [Architecture Analysis and Design Language

Paper accepted at SRDS

June 21, 2016

The paper “Model-Checking Assisted Protocol Design for Ultra-Reliable Low-Latency Wireless Networks” by Christian Dombrowski, Sebastian Junges, Joost-Pieter Katoen and James Gross has been accepted at

Two papers accepted at ATVA

June 21, 2016

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

LICS 2016 invited talk

May 20, 2016

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.](http://www-i2