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. […]
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 […]
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 […]
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 […]
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 […]
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 […]