The paper entitled “Tweaking the Odds in Probabilistic Timed Automata” by Arnd Hartmanns (Twente), Joost-Pieter Katoen, Bram Kohlen (Twente) and Jip Spel has been accepted at the 18th International Conference on Quantitative Evaluation of Systems (QEST 2021). The paper shows that two well-known techniques (digital clocks and backward reachability) for probabilistic timed automata (PTA) carry […]
The paper “PAYNT: A Tool for Inductive Synthesis of Probabilistic Programs” by Roman Andriushchenko, Milan Ceska, Sebastian Junges, Joost-Pieter Katoen and Simon Stupinsky has been accepted as tool paper at CAV 2021. The paper passed both the normal paper review as well as the artifact evaluation review. PAYNT is a tool that supports the automated synthesis of finite-state […]
The newspaper Aachener Nachrichten published the article Storm findet sicherheitskritische Softwarefehler. The article addresses Storm and its applications in industry.
The paper “A Modular Approach To Non-Deterministic Dynamic Fault Trees” by Sascha Müller, Adeline Jordon, Andreas Gerndt (all German Aerospace Center DLR, Braunschweig) and Thomas Noll has been accepted at the 40th International Conference on Computer Safety, Reliability and Security (SafeComp 2021). It presents a modular approach for synthesising recovery strategies from non-deterministic dynamic fault […]
The papers on the Storm model checker and the parameter synthesis tool Prophesy are both among the five most cited CAV papers in the period 2015-2021. CAV (Computer-Aided Verification) is a flagship conference on automated verification, in particular model checking. More details can be found here: https://scholar.google.com.au/citations?hl=en&vq=eng_computerhardwaredesign&view_op=list_hcore&venue=qgBvh59sjMQJ.2020
The paper “Automated Detection and Completion of Confluence for Graph Grammars” by Ira Fesefeldt, Christoph Matheja, Thomas Noll, and Johannes Schulte has been accepted as a tool paper at the International Conference on Graph Transformation (ICGT 2021). It presents an approach to check for a given context-free graph grammar whether the corresponding backward graph reduction […]
The papers “Latticed k-Induction with an Application to Probabilistic Programs” by Kevin Batz, Mingshuai Chen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja and Philipp Schröer and “Synthesizing Invariant Barrier Certificates via Difference-of-Convex Programming” by Qiuye Wang, Mingshuai Chen, Bai Xue, Naijun Zhan and Joost-Pieter Katoen have both been accepted as regular papers for CAV 2021. […]
The paper “Model Checking the Multi-Formalism Language FIGARO” by Shahid Khan, Matthias Volk, Joost-Pieter Katoen, Alexis Braibant and Marc Bouissou has been accepted at the 51st Annual IEEE/IFIP Int. Conf. on Dependable Systems (DSN). The paper presents a tool that enables the probabilistic model checking of FIGARO models and compares this tool to various existing […]
The paper entitled “Orbit-Finite-Dimensional Vector Spaces and Weighted Register Automata” by Mikołaj Bojańczyk, Bartek Klin and Joshua Moerman has been accepted at LICS 2021. This paper introduces a new model, weighted register automata, and shows that it has good decidability properties and that is defines a robust class of languages. This class of automata captures […]
The paper entitled “Counterexample-Guided Inductive Synthesis for Probabilistic Systems” by Milan Ceska, Christian Hensel, Sebastian Junges and Joost-Pieter Katoen has been accepted for the Formal Aspects of Computing journal. The paper presents a CEGIS approach to, mongst others, the sketching of probabilistic programs.