|Nov 26, 2003|
|EECS 498-3: Computational Logic
|How can you be sure that a hardware or software system is really correct?
This course is a chance to put logic and automata theory into action! Until recently, testing has been the only way to ``validate'' designs, especially of hardware components.The alternative approach of actually proving correctness has not been practical. But a new development in this area has changed all that: easy-to-use model checking systems. In this course we will study formal verification methods with an emphasis on model checking. You will learn to use the SMV model checking system developed at Carnegie Mellon and use it to verify a significant hardware or software system. This is your chance to learn about an emerging technology! There will be three hours of lecture and an one hour of discussion each week. Both graduate and undergraduate students welcome; prerequisites are EECS 203 and 376.
Prof. Bill Rounds [More Info]|