Abstract: Model checking is a technique of automated formal reasoning that is beginning to have a significant impact on the practice of system design and verification, especially in the computer systems field. For example, Intel Corporation has used a method based on model checking to verify the correctness of the instruction decoder in their Pentium processor, and Silicon Graphics Incorporated has used model checking to verify a key component of their multi-processor servers. We will briefly overview the field of model checking and its applications, and observe the remarkable confluence of ideas and techniques from pure and applied logic that led to the development of practical methods for hardware verification. Some of these developments, such as temporal logic and the mu-calculus, undoubtedly seemed obscure and theoretically motivated at their inception. Nonetheless, they now provide the tools and concepts that underlie a very practically motivated field.

Bio: Ken McMillan is a researcher in computer systems verification at Cadence Berkeley Labs, in Berkeley California. He holds a bachelor's degree in electrical engineering form the University of Illinois at Urbana, a master's degree in electrical engineering from Stanford, and Ph.D. in computer science from Carnegie Mellon. Formerly a chip designer and a biomedical engineer, he now works on formal methods in the design of complex systems. He is the author of the SMV system, a tool for formal system verification based on symbolic model checking, and the book "Symbolic Model Checking". Currently, his research focus is on the integration of deductive methods with enumerative techniques such as model checking.