June 30, 2014
Sergey Sazonov, who completed his master thesis on “Property preservation under bisimulations on Markov Automata” at our chair, received an award of the CS department for completing his master studies with excellent grades. Congratulations!
June 29, 2014
Our paper “Fast Debugging of PRISM Models” by Christian Dehnert, Nils Jansen, Ralf Wimmer, Erika Ábrahám and Joost-Pieter Katoen was accepted at ATVA 2014. The paper presents a new way to compute critical parts of a PRISM program by utilizing a MAX-SAT solver. This is the first approach rendering the computation of these sort of high-level counterexamples feasible for problems of practical relevance.
June 26, 2014
Joost-Pieter Katoen puts on some music at around 23:00 on Friday June 27. The entry fees are used to support students in third World countries.
June 26, 2014
The paper “Tight Game Abstractions of Probabilistic Automata” by Falak Sher and Joost-Pieter Katoen has been accepted at the conference Concurrency Theory. The paper presents game-based abstraction that is based on abstracting distributions (rather than states) and shows that this yields more accurate abstraction than state-based abstractions.
June 26, 2014
The paper “Parametric LTL on Markov Chains” by Souymodip Chakraborty and Joost-Pieter Katoen has been accepted at the IFIP TCS conference. The paper shows the undecidability of verifying a Markov chain against a parametric LTL (pLTL) formula, and studies the complexity of model checking several logical fragments of pLTL.
June 17, 2014
The paper “Minimal Counterexamples for Linear-Time Probabilistic Verification” by Ralf Wimmer, Nils Jansen, Erika Ábrahám, Joost-Pieter Katoen and Bernd Becker was accepted for publication in the journal Theoretical Computer Science. The paper thoroughly examines the possibilities for computing so-called minimal critical subsystems for Markov decision processes by means of mixed integer linear programming.
June 5, 2014
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 by means of many examples.
May 14, 2014
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 a novel technique on factorizing the occurring polynomials, this leads to high improvements in the…
Read more about Paper accepted at QEST 2014May 14, 2014
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 separation logic, while the latter presents an interprocedural dataflow analysis to…
Read more about Two papers accepted at ICGT 2014April 24, 2014
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 in classical ergodicity results about stochastic Petri nets.
March 26, 2014
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.
March 10, 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.
March 1, 2014
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”.
February 20, 2014
Our Dagstuhl Seminar on “Challenges and Trends in Probabilistic Programming” with Gilles Barthe, Andy Gordon and Annabelle McIver in April 2015, has been accepted.
September 17, 2013
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.