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.

We organize a workshop on “Bizarre Concurrency” in Aachen, together with Roland Meyer, Markus Müller-Olm and Heike Wehrheim. It will take place March 24th and 25th. Topic: new concurrency theory for modern memory models of microprocessors and geo-replicated data (consistency). See here for the Workshop Programme SPP.

Federico Olmedo joint our group! Federico did his PhD with Gilles Barthe in Madrid, Spain on probabilistic programs in security. He started as postdoc on the project “Automated Analysis of Probabilistic Programs”.

Our Dagstuhl Seminar on “Challenges and Trends in Probabilistic Programming” with Gilles Barthe, Andy Gordon and Annabelle McIver in April 2015, has been accepted.

Joost-Pieter Katoen has been appointed as a member of the renowned Academia Europaea (Academy of Europe), a European, non-governmental association acting as an Academy whose members are scientists and scholars who collectively aim to promote learning, education and research.

The Software Modeling and Verification Group (MOVES, moves.rwth-aachen.de) at RWTH Aachen University offers openings for several postdoctoral researchers in the area of    “Automated Analysis of Probabilistic Programs” Deadline for application: August 15, 2013. Starting dates: autumn 2013 and summer 2014. With about 38,000 students, 480 professors as well as 4,500 academic staff, RWTH Aachen […]