New Job Opportunities as Student Assistant
February 12, 2020
As Prof. Katoen has become the head of the ICT Profilearea, we are looking for two new student assistants. Further information can be seen in the following document: Job Information.
News
Paper in Acta Informatica
February 10, 2020
The paper “Indecision and Delays are the Parents of Failure — Taming them Algorithmically by Synthesizing Delay-Resilient Control” by Mingshuai Chen (RWTH), Martin Fränzle, Yangjia Li, Peter N. Mosaad and Naijun Zhan was accepted for publication in the journal Acta Informatica.
Four Papers at TACAS 2020
December 23, 2019
Four papers have been accepted to TACAS 2020 in Dublin in which our group is involved: “Learning One-Clock Timed Automata” by Jie An, Mingshuai Chen, Bohua Zhan, Naijun Zhan, and Miaomiao Zhang, and “Interpretation-Based Violation Witness Validation for C: NITWIT” by Jan Svejda, Philipp Berger and Joost-Pieter Katoen, and “Scenario-Based Verification of Uncertain MDPs” by Murat Cubuktepe, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen and Ufuk Topcu, and “Simple Strategies in…
Read more about Four Papers at TACAS 2020EAPLS PhD Dissertation Award 2018
December 12, 2019
We are excited to announce that Christian Hensel has won the EAPLS (European Association of Programming Language and Systems) PhD Dissertation Award 2018. His dissertation on “The Probabilistic Model Checker Storm” has been selected by an international jury among all nominated dissertations. The official announcement can be found here.
Incubator Grant for COMPASS
October 25, 2019
Anzen Engineering has been granted an ESA-BIC Incubator Grant to further develop the COMPASS 3.0 tool that has been developed by the MOVES group in close cooperation with the Embedded Systems Group at FBK Trento (Italy) in the context of several ESA-funded projects. They will further develop the COMPASS technology with the aim to open it up to engineering fields such as aviation, railway and automotive).
Paper in STTT
October 24, 2019
The paper entitled “IC3 Software Model Checking” by Tim Lange, Martin R. Neuhäußer (Siemens AG), Thomas Noll, and Joost-Pieter Katoen has been accepted for the International Journal on Software Tools for Technology Transfer (STTT). The paper introduces an extension of the IC3 verification algorithm for computer software that employs an explicit representation of a program’s control flow.
DFG Project Granted
October 21, 2019
The DFG has informed us that the project proposal “Parameter Synthesis for Reliable, Performant and Efficient Wireless Network Protocols” has been granted. The project aims at developing and using parameter synthesis techniques for probabilistic timed automata and applying them to design new, optimal variants of routing protocols in wireless networks such as AODV. Mojgan Kamali will be working on this project.
Paper at POPL 2020
October 9, 2019
The paper entitled “Aiming Low Is Harder: Induction for Lower Bounds in Probabilistic Program Verification” by Marcel Hark, Jürgen Giesl, Benjamin Kaminski and Joost-Pieter Katoen has been accepted for the 47th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2020). The paper tackles the problem of finding lower bounds of expected values / run-times of the output of probabilistic unbounded loops by establishing a tight connection between expectation transformers and stochastic…
Read more about Paper at POPL 2020Paper in LNCS 10,000
October 8, 2019
The paper entitled “The 10,000 Facets of MDP Model Checking” by Christel Baier, Holger Hermanns and Joost-Pieter Katoen just (finally) appeared in LNCS volume 10,000, Computing and Software Science: State of the Art and Perspectives.
Paper at CSL 2020
September 30, 2019
The paper entitled “Separation and Renaming in Nominal Sets” by Joshua Moerman and Jurriaan Rot (UCL, London and Radboud University, the Netherlands) has been accepted for the 28th edition in the series of Computer Science Logic (CSL 2020). Nominal sets provide a foundation for reasoning about names. They are used primarily in syntax with binders, but also, e.g., to model automata over infinite alphabets. In this paper, nominal sets are related to nominal renaming sets, which involve arbitrary…
Read more about Paper at CSL 2020Paper in Festschrift Scott Smolka
September 29, 2019
The paper “Model Checking Revamped: On the Automated Synthesis of Markov Chains” by Milan Ceska, Christian Dehnert, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen has been published in LNCS 11500, From Reactive Systems to Cyber-Physical Systems – Essays Dedicated to Scott A. Smolka on the Occasion of His 65th Birthday. The paper surveys a CEGAR and CEGIS approach towards the automated synthesis of finite-state Markov chains.
Paper in Information & Computation
September 29, 2019
The paper entitled “Deciding probabilistic simulation between probabilistic pushdown automata and finite-state systems” by Mingzhang Huang, Hongfei Fu (both from Shanghai Jiao Tong University), Joost-Pieter Katoen has been accepted to the journal Information and Computation. The paper shows that proving probabilistic similarity between a finite probabilistic transition system (specification) and a probabilistic pushdown automaton (implementationI is EXPTIME-complete.
Paper at PRDC 2019
September 16, 2019
The paper “Synergizing Reliability Modeling Languages: BDMPs Without Repairs and DFTs” by Shahid Khan, Joost-Pieter Katoen, Matthias Volk, and Marc Bouissou (EDF) has been accepted at the 24th IEEE Pacific Rim Int. Symp. on Dependable Computing, Kyoto, 2019. The paper discusses rules to transform the reliability formalism BDMPs into dynamic fault trees, applies this to a nuclear power plant benchmark, and compares analysis results obtained using BDMP and DFT techniques.
Best Paper Award at FMICS 2019
August 30, 2019
The paper “A DFT Modeling Approach for Infrastructure Reliability Analysis of Railway Station Areas” by Matthias Volk, Norman Weik, Joost-Pieter Katoen and Nils Nießen has been awarded the best paper award at the 24th International Conference on Formal Methods for Industrial-Critical Systems (FMICS 2019), Amsterdam, The Netherlands.
Paper at SEFM 2019
June 26, 2019
The paper “Formal Verification of Rewriting Rules for Dynamic Fault Trees” by Yassmeen Elderhalli (Concordia Univ.), Matthias Volk, Osman Hasan (Concordia), Joost-Pieter Katoen and Sofiene Tahar (Concordia) has been accepted at the 17th International Conference on Software Engineering and Formal Methods (SEFM 2019). The paper models a set of existing rewrite rules for DFTs in HOL4 and provides mechanized proofs with HOL of the correctness of these rules.