378 Verifying and Debugging Programs

There is a growing need for effective methods of designing correct computer hardware and software, particularly for safety critical systems such as automotive embedded systems software or for systems that are costly to recall such as microprocessors (e.g., the $500M loss by Intel on the Pentium division error.) To cope with these problems, Formal Methods have been developed based on the use of mathematical logic precision tools for specifying and reasoning about program correctness. Hardware, software, and design automation companies use formal methods to make their products more reliable and less costly to develop.

This course will survey the basic concepts of formal methods. The emphasis will be on using and applying mathematical logic plus finite state systems theory to program verification and debugging.

Prerequisite: Upper-division standing; additional prerequisites vary with the topic.

Undergraduate Program