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
Contact the staff: 15414-staff@lists.andrew.cmu.edu
Instructor: Matt Fredrikson
- Office Hours: Thursdays 4pm (Fredrikson, CIC 2126)
TAs: Di Wang, Ryan Chen
- Office Hours: 2-4pm Wednesdays (Wang, GHC 9003), 1-3pm Mondays (Chen, Gates Commons)
Lectures: TuTh 12:00-1:20pm in GHC 4307.
Announcements
Homework 6 released for extra credit, and is due on 5/1 at 11:59pm
4/22/20
Homework 5 released, and is due on 4/17 at 11:59pm
4/9/20
Lab 4 released, and is due on 5/1 at 11:59pm. There is a mandatory checkpoint on 4/20.
4/4/20
Homework 4 released, and is due on 4/5 at 11:59pm.
3/25/20
The first SAT lab has been released, and is due on 4/2 at 11:59pm.
2/23/20
Lab 2 has been released, and is due on 3/10 at 11:59pm.
2/23/20
Homework 3 has been released, and is due on 2/23 at 11:59pm.
2/12/20
Lab 1 has been posted, and is due on 2/18 at 11:59pm.
2/3/20
Homework 2 has been posted, and is due on 2/4 at 11:59pm.
1/23/20
Homework 1 and Lab 0 have been posted. Homework 1 is due at 11:59pm on 1/23, and Lab 0 is due at 11:59 on 1/30.
1/16/20
Welcome to Spring 2020! Be sure to enroll in the Gradescope section with entry code
MJ8Z24, and sign up for the Piazza section.
1/14/20