CS6217: Topics in Programming Languages & Software Engineering (Autumn 2023)¶
- Instructor: Ilya Sergey
- Lectures: Mondays, 11:00am-1:00pm
- Location: COM1-VCRM
Synopsis¶
In this course we will be looking at the state-of-the art techniques for ensuring correctness of various kinds of software. In other words, we will be learning how to formally prove that our programs do what they are supposed to do. While there is a number of techniques and approaches to achieve that goal, we will be focusing on a particular branch of formal methods for rigorous mathematical reasoning about the correctness of computer programs: so-called program logics.
Lecture Notes (Weeks 1-7)¶
The following list contains lecture notes and other reading materials (i.e., slides and papers). It is advised that you make yourself familiar with the slides in advance before the lecture.
- 1. Week 01: Introduction and Origins of Program Logics
- 2. Week 02: Hoare-Style Poofs and Loop Invariants
- 3. Week 03: Reasoning about Heap-Manipulating Programs
- 4. Week 04: Logics for Functional Programs
- 5. Week 05: Verifying Concurrent Programs
- 6. Week 06: Extensions of Separation Logic
- 7. Week 07: Program Logics for Weak Memory
Research Paper Based Seminars (Weeks 8-11)¶
Below is a list of the presentations based on research papers on program logics and program verification. Depending on the topic, presentations can be made by one or two students (see the numbers next to the topics). The presentations will take place in the order stated below. Please, choose your topic (and partner) by Week 6 of the class by following the link on Canvas.
Presenter(s) for each paper will have to prepare a 5-question quiz (aiming for 7 minutes at the beginning of their lecture) and email it to me at least a weak in advance for curation. In case of multiple papers suggested for a topic, use the paper marked with (*) for preparing the quiz.
- Week 08:
- Program Logics for Program Analysis
- Paper: Compositional Shape Analysis by Means of Bi-Abduction, 2009
- Presenter: Ivona Martinovic
- Program Logics for Reasoning about Crashes
- Paper: Using Crash Hoare logic for certifying the FSCQ file system, 2015
- Presenter: Yuxi Ling
- Program Logics for Program Analysis
- Week 09:
- Program Logics for Relational Properties
- Paper: Cartesian Hoare Logic for Verifying k-Safety Properties, 2016
- Presenter: Ali El Husseini
- Program Logics for Security
- Paper: A Separation Logic for Information Flow Control Policies, 2014
- Presenter: Hendy Liang
- Program Logics for Relational Properties
- Week 10:
- Program Logics for Resource Analysis
- Paper: Amortised Resource Analysis with Separation Logic, 2011
- Presenter: Qiyuan Zhao
- Program Logics for Under-Approximate Reasoning
- Paper: Incorrectness Logic, 2020
- Presenter: Desmond Lau
- Program Logics for Resource Analysis
- Week 11:
- Program Logics for Program Synthesis
- Paper 1*: Structuring the Synthesis of Heap-Manipulating Programs, 2019
- Paper 2: Cyclic Program Synthesis, 2021
- Presenters: Hongshi Tan, Zheng Shi
- Program Logics for Rust
- Paper 1*: Leveraging Rust Types for Modular Specification and Verification, 2019
- Paper 2: Leveraging Rust Types for Program Synthesis, 2023
- Presenters: Christopher Adrian, Guilhem Mathieux
- Program Logics for Program Synthesis
Research Project¶
A good project would be an “interesting” verified imperative data structure with a number of methods/functions along with their non-trivial specifications. Here are some data structures and algorithms that you might consider (feel free to suggest yours):
- Splay trees and Splaysort
- High-performance B or B+ tree implementation
- Scape-goat trees
- Algorithms for memory allocation and reclamation
Lost of interesting data structures to specify and verify can be found in the literature on databases. You also may want to pick a “hard” problem from LeetCode, implement it in one of the verificaiton frameworks and verify its solution with regard to logical specification paraphrasing its description given in plain English. If you plan to work alone, you may want to consider a paper-and-pencil proof of something very tricky in a logic of choice (for instance, here’s a very interesting proof of RCU correctness published as a research paper at a top conference).
The choice of a specific program logic and/or tool is up to you. In case if you are considering making your project about computer-aided reasoning, here is an incomplete list of program logic-based tools deductive verification that you might consider using (and the languages they target):
- Dafny (DSL, extracted to C#)
- F* (DSL, extracted to OCaml/Wasm)
- Why3 (DSL, extracted to OCaml)
- Prusti (Rust)
- Gobra (Go)
- Liquid Haskell (Haskell)
- Iris (Coq) (Multiple languages)
- CFML (Coq) (OCaml)
- VST (Coq) (C)
- RefinedC (Coq) (C)
- VeriFast (Java/C)
Project-based presentations will take place on Week 12.
Additional Materials¶
This course’s GitHub Organisation. It contains all the code for the demos from the lectures.
Copyright¶
Some of the lecture materials for this course are adapted, with permission, from lectures and conference presentations by the following researchers:
- Isil Dillig (UT Austin)
- Xavier Leroy (Collège de France)
- John Wickerson (Imperial College London)