Bug Catching: Automated Program Verification
Course Overview
High-profile bugs continue to plague the software industry, leading to major problems in the reliability, safety, and security of systems. This course teaches students how to write bug-free code through the process of software verification, which aims to prove the correctness of a program with respect to a mathematical specification. Along the way, students will learn how to:
- Specify correct program behavior
- Prove the correctness of their code
- Use formal semantics to reason about the soundness of proof rules
- Write practical and efficient verified code
- Use decision procedures and model checkers to reduce verification effort
Spring 2022: This course is SYNCHRONOUS REMOTE at least for the first two weeks of classes, using the ohyay platform for live lectures
Please check out the ohyay platform tips and login instructions before the first lecture
When we are back to in-person expectation (IPE) we will be in Hamerschlag Hall B131
Lectures: Tue Thu 11:50-1:10pm, 15-414 Ohyay Course Space then HH B131
Lecture Recordings: Will be available on YouTube YouTube Channel
Office Hours Locations: Either in-person only or hybrid in-person + Ohyay. See Calendar and Map of GHC5 Spaces
Instructors:
| Matt Fredrikson | mfredrik@cmu | Mon 1:30pm-3:00pm |
| Frank Pfenning | fp@cs | Wed 12:00pm-1:30pm |
TAs:
| May Li | mayli@andrew | Tue 3:00pm-4:30pm |
| Warwick Marangos | wmarango@andrew | Wed 5:00pm-6:30pm |
| Long Pham | longp@andrew | Fri 3:00pm-4:30pm |
| Victor Song | yiwenson@andrew | Mon 7:00pm-8:30pm |
Piazza: piazza.com/cmu/spring2022/15414
Gradescope: www.gradescope.com/courses/353280
Software: This course will teach students how to use the Why3 deductive verification platform. See the notes on installation and editing.
Announcements