Informatics Seminar (Perspective in Informatics 4B) 2010 - 2011

June 21 (Mon), 16:30 - 18:00 (Note: Irregular slot. No talks on June 25)

• Place:  Lecture Hall 1, Faculty of Engineering Bldg. No.10, Main Campus
• Title:  From (Graph) Theory to Practice: Automated Program Verification using Model Checking
• Speaker:  Thomas Wahl (Oxford University)
• Abstract:  A critical step in understanding social networks is to comprehend the various underlying and hidden mechanisms that generate them. Errors in software or hardware may cause computers to "hang", to compute wrong results, or simply to crash the system. Such faults cause expensive recalls and frustrated customers at best. Much worse, failing safety-relevant applications may cost human lives. The heavy reliance of our society on the correct functioning of computing devices has spurred interest in analyzing programs for possible erroneous behavior, or proving that the program is "bug-free".
  Model Checking is an automated method to check whether a program respects a given specification. The program is encoded as an annotated transition graph, which is then analyzed using graph- and automata-theoretic means for possible violations of the specification. The method, developed over the last 25 years, is successfully being used in industry today, in companies including Intel, IBM and Microsoft, to verify correctness of hardware circuits, communication protocols, and low-level system software.
  In this talk I will first introduce Model Checking from a graph-theoretic perspective. I will sketch how properties to be analyzed are expressed in temporal logic, a powerful specification mechanism custom-designed for automated verification. I will then present fundamental approaches to address the state space explosion problem, which is the major complexity hurdle facing industrial use today. In the second part of the talk, I will describe fairly recent techniques to use model checking for the analysis of software that does not permit representation using finite transition graphs. These methods have been used to weed out many errors in device driver code of the Windows operating system, leading to a substantial increase in stability of releases of the operating system over the last decade.

Kyoto University > Graduate School of Informatics > International Courses > Informatics Seminar