Bug Catching: Automated Program Verification
Course ID 15614
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 Arian 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 & Languages requirement for the Computer Science major.
Key Topics
- Rigorous reasoning applied to program correctness
- Deductive program verification
- Model checking
- Formal specification
Learning Resources
- Course notes provided by instructors
- Piazza
- Gradescope
- Autolab
- Optional textbook available digitally through the library40% Labs, 25% Written homework, 15% midterm exam, 15% final exam, 5% participation
Course Relevance
Bugs can lead to reliability, safety and security issues within systems which can cost valuable resources, especially in industry. This course develops key skills needed to develop practical software that does not suffer from these problems.
Course Goals
- Identifying and formalizing program correctness.
- Understanding how to write correct software from the ground up using formal principles.
- Apply rigorous reasoning to program correctness.
- Experience using automated tools to assist in verifying real code.
- Understanding how modern verification tools work.
Pre-required Knowledge
- Experience programming in imperative languages
- Basic understanding of contracts and invariants, as developed in 15-122
Assessment Structure
40% Labs, 25% Written homework, 15% midterm exam, 15% final exam, 5% participation
Extra Time Commitments
This course 15-614 is for graduate students. Undergraduates should enroll in 15-414.
Course Link
http://www.cs.cmu.edu/~15414/