CS6217: Topics in Programming Languages & Software Engineering (Autumn 2023)

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.

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.

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):

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.