The paper “On the Hardness of Almost-Sure Termination” by Benjamin Kaminski and Joost-Pieter Katoen has been accepted at the 40th MFCS (Mathematical Foundations in Computer Science) conference in Milano.  This paper considers the computational hardness of computing expected outcomes and deciding (universal) (positive) almost-sure termination of probabilistic programs with non-determinism.  

We are happy to announce that our tool PROPhESY: A PRObabilistic ParamEter SYnthesis has successfully passed the CAV 2015 Artifact Evaluation. The purpose of the evaluation is to provide a service by the community to help authors provide more substantial supplements to their papers so future researchers can more effectively build on and compare with […]

The paper “Conditioning in Probabilistic Programming” by Friedrich Gretz, Nils Jansen, Benjamin Kaminski, Joost-Pieter Katoen, Annabelle McIver, and Federico Olmedo has been accepted at the 31st Mathematical Foundations of Programming Semantics Conference.  The paper provides an operational and wp-semantics for an imperative probabilistic programming language with conditioning, studies their relation, and shows its usage for program […]

Friday April 24, Falak Sher successfully defended his PhD dissertation, entitled “Abstraction and Refinement of Probabilistic Automata using Modal Stochastic Games” for a jury consisting of Lijun Zhang (ISCAS Beijing, China), Stefan Kowalewski, Erich Grädel, and Joost-Pieter Katoen (all Aachen).  Falak’s dissertation is concerned with game-based abstraction-refinement in which (instead of existing works) the underlying […]

The website for this year’s Sommerfest is now live! You can find it at http://sommerfest-informatik.de. This year it is organized by our group, and will take place June 26th. The three main events, Karriere, Kluge Kopfe and Coole Party, promise to make it a great day. Visit the link if you want to know more.

Our paper “PROPhESY: A PRObabilistic ParamEter SYnthesis Tool” by  Christian Dehnert, Sebastian Junges, Nils Jansen,  Florian Corzilius, Matthias Volk, Harold Bruintjes,  Joost-Pieter Katoen, and Erika Ábrahám was accepted for publication at the 27th International Conference on Computer Aided Verification (CAV) 2015. The paper presents the tool PROPhESY, which is dedicated to model checking and parameter synthesis for parametric discrete-time Markov […]

The paper “A statistical approach for timed reachability in AADL models” by Harold Bruintjes, Joost-Pieter Katoen, and David Lesens (Airbus Defense & Space) has been accepted at the IEEE/IFIP International Conference on Dependable Systems and Networks (DSN 2015, acceptance rate 21,8%). The paper presents a statistical model checker for checking timed and stochastic AADL models against […]

The paper “Model Checking of Open Interval Markov Chains” by Souymodip Chakraborty and Joost-Pieter Katoen has been accepted at the 22nd International Conference on Analytical & Stochastic Modelling Techniques & Applications (ASMTA 2015).  The paper shows that interval MCs with open intervals can be verified by re-using techniques for closed interval MCs.

The paper “Counterexamples for Expected Rewards” by Tim Quatmann, Nils Jansen, Christian Dehnert, Ralf Wimmer, Erika Ábrahám, Joost-Pieter Katoen, and Bernd Becker was accepted for publication at the 20th International Symposium on Formal Methods (FM) 2015. The paper presents the first approaches on counterexamples for discrete-time Markov chains and expected reward properties. Methods are proposed to extract a minimal subsystem which already […]

Monday March 9, Jonathan Heinen successfully defended his PhD dissertation, entitled “Verification of Java Programs: A Graph Grammar Approach” for a jury consisting of Arend Rensink (Twente, NL), Thomas Seidl, Martin Grohe, and Joost-Pieter Katoen (all Aachen).  Jonathan’s dissertation deals with the automated verification of pointer operations in Java Bytecode programs using quantified LTL where […]