Moves News

Paper at ATVA 2018

The paper entitled “Synthesis in pMDPs: A Tale of 1001 Parameters” by Murat Cubuktepe, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen and Ufuk Topcu has been accepted for ATVA 2018 in Los Angeles. The key idea of the paper is to use advanced techniques from convex optimisation in tight combination with model checking for synthesizing parameters […]

Two papers at QEST 2018

The paper “Parameter-Independent Strategies for pMDPs via POMDPs” by Sebastian Arming, Ezio Bartocci, Krishnendu Chatterjee, Ana Sokolova, and Joost-Pieter Katoen and the paper Model Checking For Safe Navigation Among Humans“ by Sebastian Junges, Nils Jansen, Joost-Pieter Katoen, Ufuk Topcu, Ruohan Zhang and Mary Hayhoe have been accepted at QEST 2018 in Beijing. The first paper shows […]

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 Kaminski, 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, […]