模型检测(model checking)是近年来在软件和硬件验证(verification)中的一种常用且高效的技术。它在学术界和工业界都产生了巨大的影响。2008的图灵奖正是颁发给了在该领域做出开创性贡献的Edmund Clarke,Allen Emerson和Joseph Sifakis。 德国亚琛工业大学的著名学者Prof. Joost-Pieter Katoen将应邀在我室就Model checking开展一个系列讲座，欢迎大家参加！有关讲座的细节和Katoen教授的介绍见下： Times: 2:00-4:30 PM on June the 12th, 13th and 16th In 2008, the ACM awarded the prestigious Turing Award to the pioneers of model checking, Edmund Clarke, Allen Emerson, and Joseph Sifakis. Model checking has evolved in the last twenty-five years into a widely used verification and debugging technique for both software and hardware. Model checking is based on exhaustively checking whether a model of a program or hardware circuit satisfies a property, such as the absence of deadlocks,or the validity of invariants. Properties are typically described using a temporal or modal logic. This course provides an introduction to the theoretical underpinnings 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, i.e., abstraction. Finally, we discuss verification techniques for probabilistic models such as Markov chains, and Markov decision processes. Such models are used in, e.g., communication protocols, biological systems, and hardware circuits. Lecture #1: LTL Model Checking Lecture #2: CTL Model Checking Lecture #3: Abstraction Lecture #4+#5: Probabilistic Model Checking The course is based on the new textbook "Principles of Model Checking",that is co-authored with Prof. Christel Baier (TU Dresden), and which just appeared at MIT Press. ************************************************* About Professor Joost-Pieter Katoen Prof. 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 speaker of the 2nd IEEE International Symposium on Theoretical Aspects of Software Engineering. |
| 今天是： |
