- Start VPV projectAs from 1 January 2021, the VPV project has started.
Probabilistic verification computes measures of interest—such as the probability of reaching an error state, the expected accumulated reward, or the long-run average throughput—for large Markov chains or Markov decision processes described in formal modelling languages. Its applications include safety- and performance-critical systems faced with probabilistic uncertainty—communication networks, electricity grids, data centres, airplane collision avoidance—but it is also used to e.g. reason about machine-learnt agents. Probabilistic verification faced a crisis of trust after the discovery that the standard implementation of a core algorithm, value iteration, cannot actually deliver quantifiably -correct results. With this project, we aim to fully overcome that crisis, and enable probabilistic verification to again benefit our society—increasingly reliant on critical digital and cyber-physical systems—through its various applications. We develop new sound and exact probabilistic model checking algorithms to fill several gaps in their current coverage of probabilistic formalisms and measures of interest, and to gain deeper insights into what makes these algorithms (supposedly) correct. We then formalise the semantics of the JANI model interchange language and of several key algorithms, such that they can be input to an interactive theorem proving system, e.g. Isabelle/HOL. This allows us to create machine-checked correctness proofs. Based on that formalisation, we automatically derive a correct-by-construction tool guaranteed to be free of implementation bugs, and tune its performance via correctness-preserving transformations. We finally develop measure-of-interest-preserving model transformations in order to expand medium-sized models—for which our verified tool can provide knowncorrect values—into very large benchmarks that challenge even the most hand-optimised unverified probabilistic verifiers of tomorrow. At the project’s conclusion, we will have restored the trust in probabilistic verification, and set an example for other formal techniques for critical systems: they must be verified, and they can be verified.Read more
- Start SAVES project: SCALABLE VERIFICATION OF INDUSTRIAL EMBEDDED CONTROL SYSTEMSAs from 1 January 2021, the SAVES project started.
Embedded systems surround us everywhere in our everyday live. Their functionality spans from simple microcontrollers in a fridge to complex systems with millions of lines of code, for example in cars, airplanes, or smart factories. In such systems, failure often has serious consequences, such as huge financial losses or even loss of lives. Thus, the correctness and reliability of embedded systems are of vital importance. To establish correctness of embedded systems, however, is hard. With trends such as Industry 4.0, the internet of things, and autonomous driving, the complexity of embedded systems is steadily increasing. A prerequisite to ensure the correct functioning of industrial embedded systems under all circumstances is a clear understanding of the models and languages that are used in the development process. Formal methods provide a basis to make the development process systematic, well-defined, and automated. However, for many industrially relevant languages and models, the semantics are only informally defined. Together with the limited scalability of formal design and verification techniques, this makes the formal verification of industrial embedded control systems a difficult challenge, which can not be solved satisfactory with currently available methods and tools. At the same time, we see that in the area of deductive program verification, powerful techniques and tools have been developed to reason about software with unbounded parameters, for example the VerCors tool suite. In this project, we will extend these techniques with concepts to cope with heterogeneity, concurrency, and real-time to make them suitable for industrial embedded systems.
PRINCIPAL INVESTIGATORS:Read more
- Start VPV project
- Start SAVES project: SCALABLE VERIFICATION OF INDUSTRIAL EMBEDDED CONTROL SYSTEMS
- Prof. Dr. Joost-Pieter Katoen ACM Fellow 2020
- Lisandro Arturo Jimenez Roa finished his Pd Eng project on 23 November 2020
- Lukas Miedema wins 2e prize of the KNVI Thesis prize for Informatics competition
- Vincent Bloemen wins the third 2019-2020 VERSEN PhD Thesis award
- Marcus Gerhold wins the Second 2019-2020 VERSEN PhD Thesis Award
- Sophie Lathouwers wins the 2nd KNVI young talent prize
- Alice & Eve: about cool women in computing
- Wytse Oortwijn wins Best Paper Award at iFM 2019
- Mariëlle Stoelinga receives ERC Consolidator Grant
- KHMW Internetscriptie prize for Sophie Lathouwers