Bug Catching: Automated Program Verification

Catalog description

Many CS and ECE students will be developing software and hardware that must be ultra reliable at some point in their careers. Logical errors in such designs can be costly, even life threatening. There have already been a number of well publicized errors like the Intel Pentium floating point error and the Ariane 5 crash. In this course we will study tools for finding and preventing logical errors. Three types of tools will be studied: automated theorem proving, state exploration techniques like model checking and tools based on static program analysis. Although students will learn the theoretical basis for such tools, the emphasis will be on actually using them on real examples. This course can be used to satisfy the Logic and amp; Languages requirement for the Computer Science major. Prerequisites: 15-122 Min. grade C and 15-251 Min. grade C Course Website: http://www.cs.cmu.edu/~15414/