Lecture Series: Principles of Model Checking
By Professor Joost-Pieter Katoen
Times: 2:00-4:30 PM on June the 12th, 13th and 16th
Location: Room 109, Building Meng Minwei
Introduction to the Lectures
Our growing dependence on increasingly complex computer and software systems necessitates the development of formalisms, techniques, and tools for assessing functional properties of these systems. One such technique that has emerged in the last twenty years is model checking, which systematically (and automatically) checks whether a model of a given system satisfies a desired property such as deadlock freedom, invariants, or request-response properties. This automated technique for verification and debugging has developed into a mature and widely used approach with many applications. This is also witnessed by the fact that ACM recently awarded the Turing Award, the most prestigious prize in Computer Science to the pioneers of model checking, Clarke, Emerson, and Sifakis.
This course provides an introduction to the field of model checking. It covers the temporal logics LTL and CTL, compares them, and covers algorithms for model checking these logics. Techniques to combat the state-space explosion problem are at the heart of the success of model checking. We provide an overview of an important class of such techniques, namely abstraction. Finally, we conclude with model checking of systems that are subject to random phenomena, e.g., communication protocols, biological systems, and hardware circuits. We will cover the verification of Markov chains, and of Markov decision processes, i.e., models in which probabilities and nondeterminism both occur. There are altogether four lectures: (i)LTL Model Checking; (ii)CTL Model Checking; (iii)Abstraction, and (iv)Probabilistic Model Checking.
About Professor Joost-Pieter Katoen
Professor Joost-Pieter Katoen is a full professor at the RWTH Aachen University (Germany) in the Software Modeling and Verification (MOVES) group and affiliated to the Formal Methods & Tools group at the University of Twente (the Netherlands). He has done much excellent work in the area of software modeling and verification. He is visiting China as the invited talker of the 2nd IEEE International Symposium on Theoretical Aspects of Software Engineering.
