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 first paper revisits k-induction and bounded model checking (BMC) in the general…
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 analysis techniques. The FIGARO language family includes e.g., stochastic Petri nets, reliability block diagrams, and Boolean…
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 unambiguous register automata as well as probabilistic register automata.
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.
The Storm model checker received the second place at the RWTH Innovation Award 2020. An official announcement can be found here whereas a youtube video of the three winners is here (watch until the end).
The paper entitled “The Complexity of Reachability in Parametric Markov Decision Processes” by Sebastian Junges, Joost-Pieter Katoen, Guillermo Perez, and Tobias Winkler is accepted for publication in Journal of Computer and System Sciences. This paper provides several complexity results on parameter synthesis in parametric MDPs.
The paper “Scalable Reliability Analysis by Lazy Verification” by Shahid Khan, Joost-Pieter Katoen, Matthias Volk and Marc Bouissou has been accepted for the 13th NASA Formal Methods (NFM) Symposium. The paper presents an iterative method for the partial analysis of reliability (with repairs) models through lazy verification. The approach yields an upper and a lower bound on the system’s lifetime for a partial state space. The precision can be improved iteratively.
The paper “Markov Automata with Multiple Objectives” by Tim Quatmann, Sebastian Junges and Joost-Pieter Katoen has been accepted for publication in Formal Methods in System Design, a special issue for selected papers from CAV 2017. The paper presents several algorithms for automatically verifying multiple timed objectives on Markov automata, an extension of continuous-time Markov chains with non-determinism.
Joost-Pieter Katoen has been elected as new member of the Royal Holland Society of Sciences and Humanities. The KHMW was established in 1752 and is the oldest society of sciences in the Netherlands. The official announcement (in Dutch) can be found here: Benoemingen 2021
Prof. Joost-Pieter Katoen has been named ACM Fellow 2020 for his contributions to model checking of software and probabilistic systems. The ACM Fellows program recognizes the top 1% of ACM Members for their outstanding accomplishments in computing and information technology and/or outstanding service to ACM and the larger computing community. Fellows are nominated by their peers, with nominations reviewed by a distinguished selection committee. Katoen belongs to one of the 16 ACM Fellows in…
We are happy to announce that our team (Joshua Moerman and Jana Berger) has won 5 gold medals at the RERS challenge 2020. By using a combination of off-the-shelf verification tools, they have managed to crack many of the reachability problems and LTL verification problems. To get more information, please read their report.
We are delighted to inform you that three MOVES papers have been accepted at TACAS 2021: “Inductive Synthesis for Probabilistic Programs Reaches New Horizons” by Roman Andriushchenko, Milan Ceska, Sebastian Junges and Joost-Pieter Katoen “Multi-objective Optimization of Long-run Average and Total Rewards” by Tim Quatmann and Joost-Pieter Katoen, and “Finding Provably Optimal Markov Chains” by Jip Spel, Sebastian Junges, and Joost-Pieter Katoen
The paper entitled “Automated Termination Analysis of Polynomial Probabilistic Programs ” by Marcel Moosbrugger, Ezio Bartocci, Joost-Pieter Katoen and Laura Kovács has been accepted for the European Symposium on Programming (ESOP 2021). The paper presents an algebraic approach and the publicly available tool Amber to automatically prove whether a probabilistic programs is almost-surely terminating (or not) or positive almost-surely terminating (or not). It was selected as one of the 24…
We are happy to announce that the paper A Pre-Expectation Calculus for Probabilistic Sensitivity by Alejandro Aguirre, Gilles Barthe, Justin Hsu, Benjamin Kaminski, Joost-Pieter Katoen and Christoph Matheja has been selected as distinguished POPL 2021 paper. The paper develops a logic for estimating sensitivity properties (how do changes in the inputs affect the program’s output?) of probabilistic programs.
We are seeking two talented student assistants to support the digitalisation of online bridging courses in Theoretical Computer Science. More concretely, the following tasks need to be performed: the development and implementation of generators for exercise tasks and Moodle plugins and the creation of new and the preparation of existing learning material in Moodle. More details and contact addresses can be found in this announcement [in German].