The German Research Council (DFG) has granted our proposal to launch a Research Training Group on “Uncertainty and Randomness in Algorithms, Verification and Logic” (UnRAVeL). It funds 15 Ph.D. positions over a period of 4,5 years to work on challenging foundational research questions to treat uncertainty. The project involves 12 research groups from theoretical computer science, robotics, IT security, mathematics, railway engineering and business administration. The official press release can…
The papers “A Storm is Coming: A Modern Probabilistic Model Checker” by Christian Dehnert, Sebastian Junges, Joost-Pieter Katoen and Matthias Volk and “Markov Automata with Multiple Objectives” by Tim Quatmann, Sebastian Junges and Joost-Pieter Katoen have been accepted at CAV 2017. The first paper presents the new and powerful probabilistic model checker storm, whereas the second paper presents algorithms and experiments on verifying Markov automata subject to various objectives.
The MOVES group proudly announces that Professor Joost-Pieter Katoen has received a Honorary Doctorate from Aalborg University, Denmark. He was awarded for his distinguished efforts in the field of Computer Science, in particular Computer-Aided Verification. An introductory video can be found here. Award
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 reasoning about the expected values of mixed–sign unbounded random variables after execution of a probabilistic program.
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 languages, probabilistic programs, dynamic fault trees and generalized stochastic Petri nets. It has a modular set-up in which solvers and symbolic engines can easily be exchanged. It offers a Python API for rapid prototyping by encapsulating Storm’s fast and scalable algorithms. Experiments on a variety…
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 advancements,. The program will consist of presentations of work recently accepted to top conferences and ongoing work. The submissions will thus be abstracts of such work, limited to at most two pages, and will only be published in the informal pre-proceedings for the convenience of the…
It is our greatest pleasure to announce the first edition of the School on Foundations of Programming and Software systems (FoPPS). The school is jointly funded by EATCS, ETAPS, ACM SIGLOG, and ACM SIGPLAN. The topic of the first edition is Probabilistic Programming. It will take place in Braga, Portugal, May 29th – June 4th 2017. Registration: March 31, 2017 (early) and May 20, 2017 (late). Probabilistic programming languages are used for modelling and analysis purposes across multiple areas…
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, and Ufuk Topcu, and the paper “JANI: Quantitative Model and Tool Interaction” by Carlos E. Budde, Christian Dehnert, Ernst Moritz Hahn, Arnd Hartmanns, Sebastian Junges, and Andrea Turrini have been accepted at TACAS 2017. JANI consists of an intermediate model language and tool interaction protocol…
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 ESOP 2017 in Uppsala, Sweden. It introduces the concept of heap automata, a novel formalism for automatic reasoning about robustness properties of the symbolic-heap fragment of separation logic with user-defined inductive predicates.
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 Formal Aspects of Computing. The more than 50-page paper shows how graph rewriting can be applied to reduce dynamic fault trees prior to their analysis. Experiments show a speed up and memory gain of about two orders of magnitude.
The talk on “A Weakest Pre-Expectation Semantics for Mixed-Sign Expectations” has been accepted for presentation at the Probabilistic Programming Semantics (PPS) workshop at POPL’17.
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, this work considers general models evolving over uncountable…
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.
From July 25 to 28, our group hosts the Summer meeting of the AADL Standardization Committee. The Architecture Analysis and Design Language (AADL) is a modeling language for the specification, analysis, automated integration and code generation of safety-critical systems. Amongst others, it is being used in our COMPASS project for designing on-board computer-based aerospace systems.