Bug Catching: Automated Program Verification
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
Students will learn the principles and algorithms behind automated verification tools, and understand their practical limitations while gaining experience writing verified, machine-checked code that solves real problems.
Contact the staff:
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.
Homework 6 released for extra credit, and is due on 5/1 at 11:59pm
Homework 5 released, and is due on 4/17 at 11:59pm
Lab 4 released, and is due on 5/1 at 11:59pm. There is a mandatory checkpoint on 4/20.
Homework 4 released, and is due on 4/5 at 11:59pm.
The first SAT lab has been released, and is due on 4/2 at 11:59pm.
Lab 2 has been released, and is due on 3/10 at 11:59pm.
Homework 3 has been released, and is due on 2/23 at 11:59pm.
Lab 1 has been posted, and is due on 2/18 at 11:59pm.
Homework 2 has been posted, and is due on 2/4 at 11:59pm.
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.
Welcome to Spring 2020! Be sure to enroll in the Gradescope section with entry code
MJ8Z24, and sign up for the Piazza section.