CS T680 Program Verification

About This Course

CS T680: Program Verification covers selected topics in formal verification that software meets is specification. Topics this quarter will include type theory (in particular type qualifiers and refinement types), model checking, symbolic execution, Hoare logic and separation logic, model checking, and interactive theorem proving (machine checked proofs). The course will balance theoretical concerns (soundness, power) with practical concerns in applying the current state-of-the-art tools to real software.

The course will be primarily reading and lecture based, with selected programming assignments to deepen understanding.

Accessing the Readings

Some of the links above go to publisher pages, which normally ask you to pay money to access an article. DON’T DO THIS! You can get all of the articles for free, because Drexel pays for subscriptions to each of these publisher’s libraries. If you’re on campus, access should just work (you can just click the link for the PDF). If you’re off campus, go to http://vpn.drexel.edu and you can either drop the web address in an online proxy (you can see the page in a frame as if you were on campus, and therefore download the papers) or install VPN software to route your whole internet connection through campus.

Readings

There are two assigned readings for each class. You are expected to do the readings before each class, and hand in a commentary for each paper (see below) due 24 hours before each class (i.e., 6:30pm each Sunday, though you’re welcome to turn them in earlier). You turn in commentaries in a discussion forum with a thread dedicated to each paper (on Blackboard/Learn). You cannot see the contents of the thread until after you’ve posted yourself. The 24 hour window leaves time for your classmates and I to read everyone’s posts. I encourage you to respond to each others’ commentary (at any time), which will likely include questions about the papers or related work. Such discussions will improve everyone’s understanding.

Paper Commentary

For each paper you will submit a commentary that covers your understanding of the major points and contributions of the paper, the paper’s limitations, things you might not have understood (which we can explain in class!), ways to extend or improve the paper’s work, or other problems this paper’s solutions might provide insights to. Note that not all of these questions make sense for every paper we read. I mainly want to see (a) how well you understood the main ideas from the paper, and (b) that you’ve thought about how well or poorly it might really work.

More concretely, a list of things to consider in a response:

Not all of these will make sense for every paper, but most of them are sensible to cover for most papers.

Note that different people will often have different takes on the same paper, disagree on whether a choice made by the authors is a strength or weakness, or find different things clarifying or confusing. This is all okay! Everyone has different backgrounds. If you are confused about some part of the paper, don’t be shy: almost certainly someone else found it confusing, too, and maybe they’re too timid to mention it. By pointing out what was confusing or difficult, we raise the opportunity to discuss it in class and help everyone understand better. I found some parts of these papers difficult or confusing the first time (or two) I read them - this is normal.

Assignments

There will be several homework assignments / mini-projects during the quarter. Each is intended to focus primarily on getting you to apply some of the verification techniques we’ve discussed in class. There will be three moderately-sized homeworks, or 2 moderately-sized and 2 smaller assigments (for a total of 4) covering:

Grading

The course grade will be based on the homeworks and commentary:

There is no late policy for homework. If your homework is not in on time, you will receive a 0 for the assignment.

You may, at your election, skip 3 summaries during the quarter. You may skip a pair assigned for one class, or you may skip one paper one week and another paper in a subsequent week. A late summary counts as no summary; get them in on time. You must notify me when you wish to use a skip, by the time the response would be due.

If you have a legitimate reason for requesting an extension, please email me in advance to discuss unless it is an emergency.

Paper responses are graded on a scale of 0 to 3, with a divisor of 2:

The expected grade on each summary is 2; 3 is essentially a recurring opportunity for extra credit, and straight 2s is good.

Academic Honesty

Drexel University has a strict academic honesty policy. If you turn in work in this class, it must your own. You may discuss the assignments and papers with your peers if you have the opportunity, but only at the level of understanding the assignment or paper, or the logistics of getting some software installed. You are not to share code with each other. If you hand in code, writing, or other material you did not produce as if it were your own work, you are violating the academic honesty policy.

If I catch you violating the academic honesty policy, you will receive an F for the course. Period, no exceptions. Part of this process includes filing a required disciplinary report with the University. By continuing in this course, you agree to this policy.

If you aren’t sure whether something crosses the line, ask me before you do it. It is always, always, always better to ask or get a lower grade on an assignment than it is to cheat.

Schedule

HW2,Pt1HW2,Pt2
DateTopic / Reading DueSlidesOutIn
1/4Introduction to course, Type Systems
  • No reading due
HW1
1/11More types: Type Qualifiers, Refinement Types HW1,Pt1
1/18MLK Jr. Day (No class)
1/25Model Checking HW2,Pt1HW1,Pt2
2/1More Model Checking HW2,Pt2
2/8Symbolic Execution
2/15Meta: Program Verification in Practice
2/22Program Logics / Separation Logic
2/29Proof Assistants (Principles)
3/7Proof Assistants (Practice)
3/14Concurrent Programming Pick one of these data race freedom papers: AND one of: (total of 2 papers)