The paper “Multi-Cost Bounded Reachability in MDPs” by Arnd Hartmanns, Sebastian Junges, Joost-Pieter Katoen and Tim Quatmann has been accepted for TACAS 2018. The paper presemts an efficient algorithm for multi-objective model checking problems on Markov decision processes (MDPs) with multiple cost structures.
The paper “How long, O Bayesian network, will I sample thee?” by Kevin Batz, Benjamin Kaminski, Joost-Pieter Katoen and Christoph Matheja has been accepted at the European Symposium on Programming (ESOP 18). The paper shows how to use deductive program verification to deduce the expected time to obtain a single i.i.d-sample from a Bayesian network […]
On November 10 the official kick-off meeting of the Research Training Group UnRAVeL (Uncertainty and Randomness in Algorithms, Verification and Logic) will take place in room 9222, E3 Building. The program includes invited talks by the renowned researchers Prof. Marta Kwiatkowska (University of Oxford) and Prof. Rolf Möhring (TU Berlin), two-minutes talks by the UnRAVeL […]
Sebastian Junges today received the Young Research Award, a prize for excellent young researchers (students and Ph.D. students) in the ICT field, awarded by the ICT Profile Area of RWTH Aachen University. The prize comes with a financial support for Sebastian’s career.
Thursday October 19, Christina Jansen successfully defended her PhD dissertation, entitled “Static Analysis of Pointer Programs: Linking Graph Grammars and Separation Logic” for a jury consisting of Marieke Huisman (University of Twente, NL), Gerhard Woeginger, Horst Lichter, Thomas Noll, and Joost-Pieter Katoen (all Aachen). Christina’s dissertation is concerned with establishing a connection between data structure […]
The German Research Foundation (DFG) has approved to extend the funding period of the ATTESTOR project for another two-year period. The aim of the follow-up project is to develop novel techniques and tools to support formal reasoning on relational shape properties of (concurrent) pointer programs, allowing e.g. to reason about balanced tree data structures. The […]
The paper entitled “A new proof rule for almost-sure termination” by Annabelle McIver, Carroll Morgan, Benjamin Kaminski, and Joost-Pieter Katoen has been accepted for POPL 2018. The paper presents a proof rule to verify whether a probabilistic program (possibly including non-determinacy) almost surely terminates. The new proof rule enables to capture a larger class of […]
The MOVES group is co-organising a seminar on Analysis and Verification of Pointer Programs, which will be held from October 2 to 5, 2017, as an NII Shonan Meeting at Shonan Village Center in Japan. This meeting will be a scientific event bringing together both theoreticians and practitioners working on different techniques for heap abstraction […]
The paper “Conditioning in Probabilistic Programming” by Federico Olmedo, Friedrich Gretz, Nils Jansen, Benjamin L. Kaminski, Joost-Pieter Katoen and Annabelle McIver has been accepted for the journal ACM Transactions on Programming Languages and Systems. The paper treats the semantic intricacies of introducing conditioning in a probabilistic programming language, its interference with non-determinacy, and divergence.
The paper entitled “Automated Fine Tuning of Probabilistic Self-Stabilizing Algorithms” by Saba Aflaki, Matthias Volk, Borzoo Bonakdarpour, Joost-Pieter Katoen and Arne Storjohann has been selected as Prof. C.V. Ramamoorthy Best Paper Award at the 36th IEEE Int. Symposium on Reliable Distributed Systems in Hongkong. The paper presents automated techniques to find the probability distribution that […]