COMP 607: Automated Program Verification

Spring 2005

Safety-critical computers increasingly affect nearly every aspect of our lives. Computers control the planes we fly on, monitor our health in hospitals and do our work in hazardous environments. Computers with software deficiencies have resulted in catastrophic failures. The goal of formal verification is to to improve the safety and reliability of such hardware and software.

Computer-aided verification is a body of algorithms and structures applicable to the verification of hardware and software designs. It draws upon ideas and results from logic, graph theory, and automata theory, and combines theoretical and experimental aspects. In the last few years, this area has seen a dramatic expansion of activities. Today, companies such as AT&T, Lucent, Intel, SGI, DEC, Motorola, and SUN, which as recently as 6-7 years ago would have nothing to do with formal verification, cannot wait to get the most advanced tools available.

This short, hands-on course, will cover the fundamental principles and tools of computer-aided verification, from user's perspective. The basic concepts will be explained and demonstrated using the SPIN tool (http://spinroot.com/spin/whatispin.html). (The focus will be on applying computer-aided verification, rather than on understanding the underlying algorithms.)

If you are interested, please email ian@cs.rice.edu. This course is appropriate to both undergraduate and graduate students.

The material covered in this course is from a TeachLogic module developed under an NSF-funded Educational Innovation grant. It contains 8 lectures. We plan to ask attendees for extensive feedback on the content and presentation of the material.

If you are interested in taking the course, send a note to ian@cs.rice.edu.