Bug Catching: Automated Program Verification and Testing
High-profile bugs continue to plague the software industry, leading to major problems in the reliability, safety, and security of systems both large and small. Software verification aims to prove the correctness of a program with respect to a precise specification, and is an effective way to find and prevent such bugs. Building on several decades of research, this area has produced highly-automated tools and techniques that can be brought to bear in practice. This course will cover the following topics:
- Propositional and first-order logic
- First-order theories commonly used in software verification
- Satisfiability decision procedures for propositional and first-order logic with theories
- Well-founded and structural induction
- Specifications of program correctness
- Hoare Logic, verification conditions, and predicate transformers
- Techniques for proving termination
- Automated inductive verification
- Static analysis techniques for inferring useful invariants
- Software model checking and temporal logic
- Symbolic execution for testing
Instructor: Matt Fredrikson
- Office Hours: Mondays & Wednesdays 1am-12pm
- Location: CIC 2126
- Email: mfredrik@cs
TA: Ryan Wagner
- Office Hours: Tuesdays & Thursdays 1-2pm
- Location: GHC 6002
- Email: rrwagner@cs
Lectures: TuTh 10:30-11:50am in GHC 4211.
Assignments: Tentatively, there will be 6-8 assignments. Students will have approximately two weeks to complete each assignment, although this will vary depending on how much work is required to complete the assignment.
Exams: There will be two exams, a midterm and final. Tentatively, the midterm is scheduled for October 20.
Textbook: Aaron R. Bradley & Zohar Manna, The Calculus of Computation. Springer 2007. Available for free on campus network via this link.
Discussion: We will use Piazza by default for offline discussions. If you do not see the course page in Piazza, contact the course staff.
Grading: Grading will be based on assignments, midterm and final exams, and class participation. Because there is no required textbook, students' primary source of information is the lecture. Lecture notes will be made available after each meeting, but students are expected to attend class.
- 50% Assignments
- 25% Final exam
- 20% Miterm exam
- 5% Participation
Late work: Students may grant themselves at most two days worth of extensions on assignments throughout the semester. This means that one assignment could be turned in two days late without losing points, or two assignments could each be turned in one day late. Students who wish to use an extension should notify the instructor and TA via email by the original assignment deadline. Assignments turned in after the deadline without notification, or after any extensions have expired, will not be accepted.
Academic Integrity: Students are expected to complete each assignment on their own, and should be able to explain all of the work that they hand in. Copying code or proof material from other students or online sources is not allowed. However, students are encouraged to discuss assignments with each other at a sufficiently high level to avoid the risk of duplicating implementation or proof. Examples of this would be discussing algorithms and properties referred to in the assignment, helping other students with questions about a programming language or tool required to complete the assignment, discussing a general proof technique, or referring to an online source with useful information. If you have questions about whether something might be an issue, contact the course staff before discussing further. Please refer to the Carnegie Mellon Code for information about university policies regarding academic conduct.
Take care of yourself: Do your best to maintain a healthy lifestyle this semester by eating well, exercising, avoiding drugs and alcohol, getting enough sleep and taking some time to relax. This will help you achieve your goals and cope with stress. All of us benefit from support during times of struggle. You are not alone. There are many helpful resources available on campus and an important part of the college experience is learning how to ask for help. Asking for support sooner rather than later is often helpful. If you or anyone you know experiences any academic stress, difficult life events, or feelings like anxiety or depression, we strongly encourage you to seek support. Counseling and Psychological Services (CaPS) is here to help: call 412-268-2922 and visit their website. Consider reaching out to a friend, faculty or family member you trust for help getting connected to the support that can help.