Vortragende(r): Prof. Dr. Joost-Pieter Katoen
Achtung! Kolloquium ausser der Reihe!
Das Kolloquium beginnt bereits um 16 Uhr c.t. !
Model checking is an automated verification technique that actively
is applied to hardware and software design. Companies like IBM and
Cadence developed their in-house model checkers, and acted as driving
forces behind the design of the IEEE-standardized temporal logic PSL.
On the other hand, model checking C-, C#- and .Net-program code is an
intensive research topic at, for instance, Microsoft and NASA.
Another indication for the importance of model checking is the fact
that their originators received the ACM Turing Award 2007.
In this talk, we discuss three non-standard applications of model
checking. The first example is taken from systems biology and shows
the relevance of (probabilistic) reachability. Then, we show how to
determine the optimal scheduling policy for multiple-battery systems.
Finally, we discuss a stochastic scheduling problem that --thanks to
recent developments-- can be solved using model checking.
Joost-Pieter Katoen is a full professor at the RWTH Aachen University
and is part-time associated with the University of Twente, The Netherlands. His research interests include concurrency theory, model checking, timed, stochastic and hybrid systems, and semantics. He co-authored more than 140 journal and conference papers, and co-authored the comprehensive book Principles of Model Checking (with Christel Baier). He is a member of the IFIP WG 1.8, IEEE Computer Society and senior member of the ACM.