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
Lectures: Tue Thu 12:30-1:50pm, HH B131
Instructors:
Ruben Martins | rubenm@andrew.cmu.edu | OH: Wednesdays @ 2pm GHC 7129 |
TAs:
Cayden Codel | ccodel@andrew.cmu.edu | OH: Fridays @ 1.30pm GHC5 Table 2 |
Pratap Singh | prataps@andrew.cmu.edu | OH: Mondays @ 3pm CIC 2201 |
Tony Yu | tonyy@andrew.cmu.edu | OH: Thursdays @ 5pm GHC5 Carrel 1 |
Ying Sun | yingsun@andrew.cmu.edu | OH: Tuesdays @ 2pm GHC5 Table 4 |
Piazza: piazza.com/cmu/spring2023/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
Assignment 5 has been posted and is due at 11:59pm on 3/22.
3/15/2024
Assignment 4 has been posted and is due at 11:59pm on 3/15.
3/4/2024
Mini-Project 1 has been posted. The checkpoint is due at 11:59 pm on 2/23 and the final submission is due at 11:59 pm on 3/1.
2/16/2024
Assignment 3 has been posted and is due at 11:59pm on 2/16.
2/9/2024
Assignment 2 has been posted and is due at 11:59pm on 2/9.
2/2/2024
Assignment 1 has been posted and is due at 11:59pm on 2/2.
1/26/2024
Assignment 0 has been posted and is due at 11:59pm on 1/26.
1/19/2024
Welcome to Spring 2024! Be sure to check you are enrolled in
Gradescope and Piazza.
1/16/2024