Moves News

Paper at SUM 2018

The paper entitled “Rule-based Conditioning of Probabilistic Data Integration” by Maurice van Keulen, Benjamin Kaminski, Joost-Pieter Katoen, and Christoph Matheja has been accepted for the 12th Int. Conf. on Scalable Uncertainty Management. The paper presents  how to integrate evidences into a probabilistic database.

Positions for PhDs and postdocs

We solicit applications for PhD studentships and postdoctoral research positions in the area of verifying probabilistic programs. The positions are funded by the recently acquired ERC Advanced Grant “Formal Reasoning about Probabilistic Programs (FRAPPANT)”. What is this project all about? Probabilistic programs describe recipes on how to infer statistical conclusions about data from a complex […]

Paper at UAI 2018

The paper entitled “Finite-State Controllers of POMDPs using Parameter Synthesis” by Sebastian Junges, Nils Jansen, Ralf Wimmer, Tim Quatmann, Leonore Winterer, Bernd Becker, and Joost-Pieter Katoen has been accepted for the Uncertainty in AI 2018 Conference in Monterrey, USA. The key idea of the paper is that that computing randomised FSCs on POMDPs is equivalent […]

Paper at SPIN 2018 Symposium

The paper entitled “Improving Generalization in Software IC3” by Tim Lange, Frederick Prinz, Martin R. Neuhäußer (Siemens), Thomas Noll and Joost-Pieter Katoen has been accepted for the 25th International Symposium on Model Checking of Software (SPIN 2018) in Malaga, Spain. The paper presents several advancements to the generalization procedure of IC3, focused on software verification. […]

Paper in Acta Informatica

The paper entitled “On the Hardness of Analyzing Probabilistic Programs” by Benjamin Kaminksi, Joost-Pieter Katoen, and Christoph Matheja has been accepted for publication in the journal Acta Informatica. The papers presents various hardness results for elementary decision problems on probabilistic programs such as “does a program terminate almost surely?”, “does it terminate in finite expected […]

Paper in Journal of the ACM

The paper entitled “Weakest Precondition Reasoning for Expected Runtimes of Randomized Algorithms” by Benjamin Kaminski, Joost-Pieter Katoen, Christoph Matheja and Federico Olmedo has been accepted for the prestigious journal Journal of the ACM. This paper presents a wp–style calculus for obtaining bounds on the expected run time of randomized algorithms.Its application includes determining the (possibly […]

Two papers accepted at FM 2018

The papers “Verifying Auto-Generated C Code from Simulink” by Philipp Berger, Joost-Pieter Katoen, Erika Ábrahám, Md Tawhid Bin Waez and Thomas Rambow, as well as the paper “Formal Verification of Automotive Simulink Controller Models: Empirical Technical Challenges, Evaluation and Recommendations” by Johanna Nellen, Thomas Rambow, Md Tawhid Bin Waez, Erika Abraham and Joost-Pieter Katoen, have […]

Paper accepted at SEFM 2018

The paper “Graph-Based Shape Analysis Beyond Context-Freeness” by Hannah Arndt, Christina Jansen, Christoph Matheja and Thomas Noll has been accepted for publication at the 16th International Conference on Software Engineering and Formal Methods (SEFM 2018). It introduces a shape analysis for reasoning about relational properties of data structures that are maintained by a pointer program, […]

Katoen receives ERC Advanced Grant

Joost-Pieter Katoen is awarded the prestigious ERC Advanced Grant from the European Research Council. It will allow to fund a project on formal reasoning techniques for probabilistic programs over a period of five years. ERC Advanced Grants are intended to support the very best research to be conducted in EU member states and associated countries. […]

Four Papers at CAV 2018

Four papers with involvement of the MOVES group have been accepted at CAV 2018: “Sound Value Iteration” by Tim Quatmann and Joost-Pieter Katoen “Let this Graph be your Witness! An Attestor for Verifying Java Pointer Programs” by Hannah Arndt, Christina Jansen, Joost-Pieter Katoen, Christoph Matheja and Thomas Noll “Monitoring CTMCs By Multi-Clock Timed Automata” by […]