Course Syllabus and Policies¶
Goals and High-Level Agenda of the Course¶
Program logics allow us to specify and prove what a program should do in the same way ordinary logics allow us to make statements about phenomena occurring in a regular world. Using program logics for specifying program behaviour comes with multiple advantages. First, proofs in such logics are fully formal and can be easily checked, either manually or via a specialised checker software—thus removing the need to trust the verifier. Second, reasoning in program logics is often can be done compositionally, i.e., in a divide-and-conquer fashion reminiscent to ordinary programming, where functions are built of other functions or primitive operations. For instance, in order to verify a large piece of software, one can first ascribe some specifications to the libraries it uses and verify that the libraries satisfy them, and then use those library specifications (but not the libraries themselves) to verify the “main” program. This idea can be, of course, used iteratively, verifying the program “in layers”.
While the idea of program logics comes from 1960s, it took several decades to make it scale for programs with “non-trivial” language features, such as pointer arithmetic, concurrency, randomness. Furthermore, in the recent decades more program logics have been designed to verify distributed systems, probabilistic and quantum programs, as well as to design trustworthy bug-detectors and verify compiler optimisations.
In the first half of this class, structured as a series of lectures, we will study the “classic” ideas in programming logics, starting from verification of simple imperative programs, thread-based concurrency, program with pointers and touching upon topics related to reasoning about presence of bugs and relational (i.e., multi-program) specifications. The second half of the course will be dedicated to you presenting state-of-the art papers on program logics.
A large part of the course’s assessment will be dedicated to conducting a project on using one of modern program logics for verifying a small but “interesting” program. Possible topics of the projects will be announced by the Week 4 of the term and listed below on this page. In the last couple of weeks, we will will have presentations, in which you explain the chosen problem and the formal development.
Topics and Lectures¶
The tentative list of lecture topics below is a subject of possible minor changes.
- Origins of formal verification. Proof about programs using program logics. Floyd-Hoare Style reasoning.
- Loop invariants. Soundness and completeness of Hoare logic. Weakest precondition calculus.
- Separation Logic (SL) and reasoning about programs with pointers.
- Reasoning about functional programs. Mechanically verifying OCaml programs with Separation Logic in a proof assistant (CFML/Coq, F*).
- Verification of Concurrent Programs. Concurrent Separation Logic (CSL).
- Extensions of Separation Logic: magic wands, fractional permissions, permission algebras, ghost code. Owicki-Gries reasoning.
- Program logics for relaxed consistency and concurrency
Paper-Based Presentations & Quizzes¶
In the second half of the course (weeks 8-11), we will have several presentations based on the research papers. Each of you will have to choose a topic to present, and 1-3 papers that cover that topic well. Your goal is to produce a presentation that is a coherent overview of the main ideas and the state of the art, supported by illustrative examples and high-level intuition on the proof principles.
Paper-based quizzes. As a part of your preparation for the presentation, you will have to prepare a 5-question mini-quiz (for 10 minutes) based on the material of the papers you’ll be reading and send it to me one week before your talk. I will assess the quality of your quiz and assign part of your grade based on it. The quiz will be then offered to all other students in the class at the end of your presentation.
The following list provides potential topics for presentations (one bullet point is one topic, assuming one or more papers). The list will grow as I come up with more themes to present. You are also welcome to propose a topic that is not in the list, but I will have to approve it for presentation before assigning it to you. You will have to finalise your decision by the Week 6 of the course.
Research Projects¶
The projects can be tackled individually or in pairs. In the case of a pair project, I will expect a mechanisation artefact (i.e., machine-checked proofs) that implements the specification and verification task, while single-person projects can provide paper-and-pencil formal development.
Grading Schema¶
The final grade is combined from the following components:
Engagement during the Lecture Weeks: 5%
Paper-Based Quizzes: 10%
This part will be determined by your answers to the quizzes proposed by other students for their respective papers.
Paper-Based Presentations: 25%
This part of the grade will be determined by the quality of your presentation based on a research paper. The grade is formed as follows:
- 15%: Quality of the talk: how easy is it to follow and how well does it explain the paper’s main ideas.
- 5%: Answering the questions from the audience.
- 5%: Quality of the prepared quiz based on the paper.
Research Project: 60%.
- Initial project proposal: 10% (why the problem is interesting, why feasible)
- Written report: 20% (evaluated based on structure, clarity)
- Presentation: 20% (you should be able to explain your design choices)
- Self- and peer evaluation: 10% (based on the peer feedback in case of teams of two)
The following cutoffs will be used to determine letter grades. In the ranges below, x stands for your total score at the end of the semester. Final scores near a cutoff will be individually considered for the next higher grade. Plus(+) and minus(-) grades will also be given; their cutoffs will be determined at the end of the semester.
| Score | Grade |
|---|---|
| 88 ≤ x < 100 | A |
| 75 ≤ x < 88 | B |
| 60 ≤ x < 75 | C |
| 50 ≤ x < 60 | D |
| 0 ≤ x < 50 | F |
Grades are not curved. It is theoretically possible for everyone in the class to get an A (or an F). Your final grade depends only on your own final score and not on that of others.