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 the study 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 5-6 years ago would have nothing to do with formal verification, cannot wait to get the most advanced tools available, and many of them have formed R&D groups to develop verification software tools and apply them to their own designs. In addition, several commercial tools have been announced over the last couple of years. As tool creation is driven directly from the theory, this creates an unusual opportunity to see theory put directly to practice, a stimulating and attractive reward.
The seminar will serve as a participatory introduction to this dynamic research area. We will meet weekly and read together a doctoral dissertation covering the theoretical and practical aspects of computer-aided verification.