CpSc 538G: Formal Verification and Analysis -- Reading List

This list will certainly change as the term progresses. My approach is to start topics with papers that were aimed at a general, computer science, audience, and then follow up with deeper papers from the research literature. Some of the research papers are long, dense, or both, and we won't actually cover the material in a single class session. Also, I want to do examples on the white board or on the computer. So, I'll adjust the schedule to make room as we go along. I'll note the changes in class, but you should come back to this page to check if you're not sure what we'll be covering.

The URLs that I'm including for the papers use UBC ezproxy links when I could find them. If the proxy isn't working for you, click here to log-in. If you're not from UBC but reading this because you want references on formal verification, that's great! I'll try to remember to include links without the proxy -- if I forget, you can just delete the .ezproxy.library.ubc.ca stuff from the URL.

Formal verification is progressing very rapidly both in research and in applications. There's no way we'll cover the whole field in one term. To help make up for some of the inevitable gaps, I've suggested papers "For further reading" throughout this list.

I've borrowed extensively from the excellent reading list that Alan Hu created for earlier offerings of this course. Feel free to check out the original. Alan has some insightful commentary, and he lists some papers that aren't on this list -- in case your looking for something in a category that I've missed.

Welcome to Formal Methods for Analysis and Verification

September 6:

September 7:

SMT is cool, and we can use it to find bugs.

September 12:

September 14:


Choose one of the two papers below to read (and write a short review):

SAT solving: methods and applications

September 19: The DPLL algorithm

For further reading (optional):

September 21: Binary Decision Diagrams

For further reading (optional): Carl Seger's Guest Lecture

September 26 & 28: Efficient SAT Solvers

For further reading (optional):

Model Checking

October 3:

For further reading (optional):

October 5:

For further reading (optional):

October 12 & 17:

October 19:

SMT Solvers

October 24:

For further reading (optional):

Symbolic software execution

October 26:

For further reading (optional):

October 31:

For further reading (optional):

November 2:

Interpolation

November 7:

November 9:

IC3 For further reading (optional):

November 14:

Theorem Proving For further reading (optional):

November 16:

Machine Learning

November 21:

November 23:

Cyber-Physical Systems

November 28 & 30:

The first paper sets the stage for some of the important reasons why we should care about cyber-physical systems. The second paper is much more technical -- it both shows how verification can be applied to a real-world control system, and it shows (although, not necessarily obviously), how the AI monitors of the first paper might be included in a real controller.

Beyond this reading list

My goal in teaching CPSC 538G is to provide an introduction and overview of formal methods. There is much more to the field than can be covered in one term. Fortunately, we may be able to cover a bit more than the topics on the list above. Each student in the course is expected to present a paper. You can Last modified (GMT)