If you designed a new system or protocol, would you sign a liability contract guaranteeing that your design met its requirements? Do you wish that software and hardware companies would replace disclaimers with warranties? (wording adapted from D.L. Parnas)

Synopsis: As computer systems and protocols grow increasingly complex, detecting errors in their designs becomes increasingly difficult. The growing use of computer systems in safety-, life-, and financially-critical applications demands validation techniques that guarantee the absence of certain classes of errors. Testing, however, can never guarantee that systems are error-free. What's a designer to do?

Computer-aided verification complements conventional testing with techniques for formally proving that designs satisfy certain behavioral requirements (such as "every request is eventually acknowledged"). Major semiconductor companies use these techniques on many systems, including cache coherence protocols, floating point units, communication protocols, and pipelined architectures. Agencies such as NASA use these techniques to validate aspects of critical systems (such as deep space probes).

This seminar will explore the theory and practice of computer-aided verification. We will study techniques for modeling systems and specifying and verifying their behavior. This year, the course will focus on modeling and specifying software systems, though we may look at simple circuits and protocols at the start of the semester for comparison. Assignments will involve paper reading and presenting, pencil and paper exercises, and using software tools to verify designs.