Syllabus

Bug Catching: Automated Program Verification

Contact the staff: 15414-staff@lists.andrew.cmu.edu

Instructors: Matt Fredrikson and André Platzer

TAs: Jonathan Laurent, Tianyu Li

Lectures: TuTh 10:30-11:50am in GHC 4211.

Software: This course will teach students how to use the Why3 deductive verification platform, and the Spin model checker. Installation instructions will be provided with the labs that use this software.

Course textbook

There is no textbook for this class. Lecture notes will be posted to the course website but do not always contain everything covered in class. Comments and corrections are welcome, please give them to the course staff on Piazza.

Course schedule

Consult the online schedule for up-to-date information.

Learning objectives

Identify and formalize program correctness. In order to reason about the existence of bugs in code, and ultimately justify their absence, we need to state what it means for the code to be correct. Students will learn how to formalize correctness using logical specifications that give precise meaning to the program's intended behavior.

Understand how to write correct software from the ground up. Writing good specifications of program correctness is essential to showing that there aren't any bugs in the code, but it is also useful for writing good code from the start. Students will develop experience reasoning about correctness as they implement functionality, learning how to write code that establishes and preserves properties and invariants needed to meet a target specification.

Apply rigorous reasoning to program correctness. Program verification is the process of mathematically proving that all possible behaviors of a given program adhere to its specification. Students will learn how to use deductive reasoning and state space exploration to realize this goal, and gain experience verifying their own code against logical correctness specifications.

Learn to use automated tools to aid in verification. Formally verifying real code is challenging, but given the scale of modern software, can also be tedious and labor-intensive. A number of tools exist for automating key parts of the verification process, notably deductive verification tools and model checkers. Students will learn how to use these tools when developing correct software, and gain experience applying them to non-trivial implementations.

Understand how verification tools work. Verification tools are not perfect, and will never be able to scale universally to all software development needs. Understanding the principles and techniques that these tools use is necessary for evaluating when it is appropriate to use a particular tool, and for addressing a tool's limitations when they arise in practice.

Lectures

We enjoy seeing you in class, so please come to the lectures unless you have an unavoidable conflict, in which case you are expected to follow up with what you have missed in class on your own. Although class participation only counts for a small portion of your grade, it can be enough to sway a final letter grade in certain circumstances. Please sit near the front, interact, and ask questions. This is the best way to learn!

As research on learning shows, unexpected noises and movement automatically divert and capture people’s attention, which means you are affecting everyone’s learning experience if your phone, laptop, etc. makes noise or is visually distracting during class. You may use laptops for taking notes, but if the course staff notices other content on your screen that may be distracting for you or others—news, videos, games, or even other homework—we will ask you to put the device away for the rest of the lecture.

Assignments, exams, and grading

Grading will be based on labs, written homework, midterm and final exams, and class participation. Barring exceptional circumstances, letter-grade thresholds are: 90% (A), 80% (B), 70% (C), 60% (D).

Labs (40%)

The lab assignments are designed to give you hands-on experience writing bug-free code with the help of formal verification tools. We will cover two such tools: a deductive verification platform (Why3), and a model checker (Spin). In general, the labs will ask you to implement some interesting functionality, such as a SAT solver or fault-tolerant communication protocol, provide a formal specification of what it means for that functionality to be correct, and use the appropriate tool to verify that you have implemented it correctly. For many this is likely to be the most challenging part of the course, but it will also be rewarding. The experience of writing a complex program, proving it correct, and having it work exactly as intended on the first execution (and all subsequent ones) is exhilarating!

The most important criterion with respect to grading the labs is correctness. An ideal lab attempt contains concise, correct specifications and sufficient proof annotations for the automated verifier to certify correctness. This will receive full credit, in addition to pleasing the course staff as the verifier will do most of the work in grading. However, it may be the case that your specification is incorrect, or too complicated for the grader to fully understand. Verification cannot be fully automated, and finding the right annotations to provide to the tool can be challenging, so it can happen that you do not provide a solution that the verifier can certify (even if you implemented the functionality correctly). In these cases, you will receive partial credit, so it is also important that the code you hand in be clean and well-commented, as course staff cannot assign points to solutions that they do not understand.

Labs will be handed in on Autolab.

Homework (25%)

Written homework will be assigned more frequently, and should not require as much time to complete as the labs. The goal of the written homework is to help you refine the fundamental skills, and better understand the theoretical underpinnings, that you will need in order to do well on the labs and exams. Grading for these assignments is based on the correctness of your answer, and the presentation of your reasoning. You should strive for clarity and conciseness, while making sure to show each step of your reasoning. Categorical answers with no explanation will not even receive partial credit, but lucid explanations of your attempt to find the answer will.

Written homework will be handed in via Gradescope, and should preferably be typeset in LaTeX. Homework that the course staff cannot read cannot obtain any points.

Exams
(15% midterm, 15% final)

We will have two in-class exams. The content of these exams will more closely resemble the written homework than the labs, but some questions may rely on, or make reference to, key parts of the labs. The midterm will take place during the normal class meeting time, in the same room used for lectures. Both exams are "closed book" (i.e., you may not reference our lecture notes), but you are allowed to bring a single double-sided sheet of hand-written notes.

For special accommodations on exams, students should submit an accommodations letter to the course staff at least one week before. For extra time on exams we then ask that you arrange it to be proctored through the disability services office (assuming you have given us the form) for each exam separately. We will work with them to get them a copy of the exam. For other issues please contact the instructor. No make up exams are given, except for medical reasons. To schedule a make-up exam, ask your academic advisor to contact the instructors. Please do not email the course staff personally. You will need to provide medical documentation that shows that you cannot take the exam.

Participation (5%)

Active class participation counts for a small percentage of your grade, and in borderline letter-grade cases, could be decisive of what ultimately appears on your transcript. This is a relatively small course, so we expect to become familiar with each of you through your lecture attendance. Some factors that we will use to decide the participation component are interaction through good questions and answers during class discussions. Although you are not required to make use of Piazza, we appreciate students who are willing to help others by answering questions and providing helpful advice, and doing so will factor into your participation grade positively.

Late Assignments

Proving correctness of real code can be difficult, even when you have correctly specified and implemented the functionality. To give you the opportunity to earn back points that you might have missed by not successfully verifying your code, you can resubmit each lab once within three days of the original due date. However, you will only gain points for the proof portion of the lab—you will not get points after the deadline for changes made to your implementation or specification. To earn any points after the deadline, your proof must be complete, and the verifier must accept it.

There are no late days for written homework. If you submit a written homework after the assigned deadline, your grade will be docked 25% for each late day.

Communication

When you need help from the course staff, please use Piazza first. If you feel that Piazza is not appropriate, then you can email us at 15414-staff@lists.andrew.cmu.edu. Please refrain from emailing professors or individual TAs, except in cases that require privacy. Of course you are always welcome to office hours, or to ask the TAs or professor questions after class, time permitting.

How to use Piazza: We will post announcements, clarifications, corrections, and hints on Piazza, and in certain cases to the course webpage. When using Piazza for discussion of labs and homework, please resist the temptation to ask every question that you might have. Even with a moderately-sized course like this one, the volume of traffic can get out of hand, making it difficult for course staff and other students to keep up. Most importantly, the best way to learn this material is to spend time thinking through the details yourself, and exploring various alternative solutions. Asking others for too many hints contradicts that process, and will leave you less well-prepared for exams and future labs.

Please make your Piazza questions public. Chances are that other students have similar questions to the one you're asking, and marking it private will likely require the course staff to spend unnecessary time posting responses to several minor variations of the same question. A good heuristic to use is that if you don't feel comfortable making your question public, then Piazza might not be the right place to ask it. In these cases, emailing the course staff, or coming to office hours, may be the right thing to do.

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.

Accessibility

Carnegie Mellon University makes every effort to provide accessible facilities and programs for individuals with disabilities. If you have a disability and require accommodations, contact the Office of Disability Resources at access@andrew.cmu.edu. Please let the instructors know early in the semester so that your needs may be appropriately met. Special accommodation for exams must be requested for each exam separately one week in advance.

Take Care of Yourself

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. You should ask sooner rather than later. Should you find yourself or a friend in serious trouble, take it seriously: your classes can wait. For emergencies call UPMC’s re:solve Crisis Network at 1-888-796-8226. Counseling and Psychological Services (CaPS) is here to help: call 412-268-2922 and visit their website at http://www.cmu.edu/counseling/. Also consider reaching out to a friend, faculty or family member you trust for help getting connected to the support that can help.