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 […]
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 al gorithms.Its application includes determining the […]
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 […]
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, […]
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 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 […]
The paper “Branching Bisimulation and Concurrent Object Verification” by Xiaoxiao Yang, Joost-Pieter Katoen, Huimin Lin, Gaoang Liu, and Hao Wu has been accepted for the 48th IEEE/IFIP International Conference on Dependable Systems and Networks (DSN 2018) in Luxemburg. The paper, a result of the cooperation within the CDZ project CAP with the Institute of Software, […]
The paper “One Nets Fits All — A unifying semantics of Dynamic Fault Trees using GSPNs” by Sebastian Junges, Joost-Pieter Katoen, Marielle Stoelinga and Matthias Volk has been accepted for Petri Nets 2018. The paper presents a simple, compositional GSPN semantics for DFTs that unifies all existing DFT semantics from the literature.
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 presents 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 […]