Abstract

With their ever increasing size and complexity, functional correctness has become one of the major concerns in the design and implementation of modern computer systems. Formal verification (or FV, for short) seeks to validate functional correctness by employing techniques that are more exhaustive and mathematically rigorous than traditional testing and simulation. While by no means a panacea, FV has been successfully applied to many real-world verification problems in the last decade or so. In this talk I will try to give you a taste of FV by presenting three FV techniques and their successful industrial applications: binary decision diagrams/circuit equivalence checking, symbolic model checking/cache coherence protocol verification, and mechanical theorem proving/floating-point hardware verification. Needless to say, one lecture is too short for even one of these topics. Those interested are encouraged to take my course "Computer-Aided Formal Methods", which is to be offer in Spring 2003 and whose web page is at: http://home.pacbell.net/ctchou/scu-cafm.html.

Biography

Ching-Tsun Chou is a Platform Architect and Verification Engineer at Intel Corporation, where he applies formal methods to the design, definition, and verification of complex protocols used in distributed shared memory systems. Earlier he was a Verification Engineer in Intel's Itanium processor design team, where worked on both formal and simulation-based hardware verification, and a VLSI CAD Researcher in Fujitsu Labs of America, where he worked on the application of synchronous programming languages to hardware design. He has published a number of papers on formal verification, synchronous programming, and distributed algorithms and served on the program committees of several international conferences on formal verification. He earned a Ph.D. degree in Computer Science from UCLA and has one patent pending.