Department of Computer Science
CPSC 513: Introduction to Formal Verification and Analysis

Assigned Readings:

I'm always tweaking the reading list, so this list will mutate over time. Also, I'm building on many old reading lists, so if you go read the commented-out HTML, you'll see old readings listed. Some of those we'll use, but some we won't. (But they're all good papers...)

Week 0:

These two papers are optional, and you haven't learned enough to understand most of the details yet (You will!), but these are nice ways to get motivated, by seeing impressive industrial case studies that show successful adoption of modern, automated, formal verification techniques. For now, just skim over anything that doesn't make sense (or google/wikipedia them if you're curious), and concentrate on the results!

Alternatively (also optional), the 2007 Turing Award Lecture by Clarke, Emerson, and Sifakis gives a surprisingly concise overview of most of the material in this course: (Most paper links I post are from the publisher's websites. This is the most "proper" place to link to, but the publishers are generally behind pay walls. Fortunately, if you're accessing from a UBC machine, the UBC Libraries have negotiated site-wide access for you, so you can download the paper for free from UBC machines. Let me know if you have any trouble with this.)

Week 1:

Randal E. Bryant, "Symbolic Boolean Manipulation with Ordered Binary Decision Diagrams", ACM Computing Surveys, Vol. 24, No. 3 (September 1992), pp. 293-318. (Preprint published as CMU CS Tech Report CMU-CS-92-160.) Sections 1 to 3 are the relevant ones for us, although the whole paper is excellent. Here is a link to the official version at the ACM Digital Library. You have free access from UBC machines.

Karl S. Brace, Richard L. Rudell, and Randal E. Bryant, "Efficient Implementation of a BDD Package", 27th Design Automation Conference, pp. 40-45, 1990. How BDD packages are really implemented. (Optional.)

Randal Bryant, "On the Complexity of VLSI Implementations and Graph Representations of Boolean Functions with Applications to Integer Multiplication", IEEE Transactions on Computers, Vol. 40, No. 2, February 1991. A general technique for proving BDDs big for certain functions (and getting better intuition about what makes BDDs big). (Optional. You may find this interesting if you like theory and/or are interested in understanding what makes BDDs blow up.) Here is additional explanation of the combinatorial part of Bryant's multiplication proof. Optional

I hope we'll have time to take a quick look at cutpoints for combinational equivalence. Here are some of the classic references on practical techniques for scaling combinational equivalence checking up to practical sizes. (These are all optional.)

Week 2:

Lintao Zhang and Sharad Malik, "The Quest for Efficient Boolean Satisfiability Solvers", Invited Paper, Proceedings of 14th Conference on Computer Aided Verification (CAV2002), Copenhagen, Denmark, July 2002, Springer Lecture Notes in Computer Science Volume 2404, pp. 17-36. (Also in Proceedings of 8th International Conference on Computer Aided Deduction (CADE 2002).) A good survey of the big breakthrough in complete SAT solving for verification applications, about 15 years ago.

Here is additional explanation of implication graphs and learning. Optional

My notes above were based in part from this additional paper: Lintao Zhang, Conor F. Madigan, Matthew H. Moskewicz, Sharad Malik, "Efficient Conflict Driven Learning in a Boolean Satisfiability Solver", ICCAD 2001, pp. 279-285. Optional

Lintao Zhang and Sharad Malik, "Validating SAT Solvers Using an Independent Resolution-Based Checker: Practical Implementations and Other Applications," DATE 2003, pp. 10880-10885. This is the classic paper on getting a proof out of a modern SAT solver. It's also a nice description and proof of correctness of the algorithm used in current SAT solvers. Optional

Week 3:

C. A. R. Hoare, "An Axiomatic Basis for Computer Programming", Communications of the ACM, October 1969, pp. 576-583. This is a classic paper on the basic ideas of software verification. From UBC machines, you'll see a link for the full-text PDF.

Edsger W. Dijkstra, "Guarded Commands, Nondeterminacy, and the Formal Derivation of Programs," Communications of the ACM, 18(8), August 1975, pp. 453-457. Another classic on the foundations of software verification. This paper gets a bit ahead of ourselves, as we'll see guarded commands and non-determinism later, but this introduces weakest precondition. From UBC machines, you'll see a link for the full-text PDF.

R. W. Floyd, "Assigning Meanings to Programs", Proceedings of Symposia in Applied Mathematics, Vol. 19, 1967, pp. 19-32. This is the true original. I can't find an official copy on-line, but there are some scanned copies on-line, e.g. here . I also have an official hardcopy reprint and can make copies if anyone is interested. (Back in the old days, before the Internet or even laser printers became widespread, when you published a paper, the publisher would send you a fixed number of printed copies of your paper, called "reprints". If someone wanted a copy of your paper and didn't have access to the journal in a nearby library, they'd send you a physical mail request for a reprint, and you'd physically mail them a copy. I have an official reprint that Bob Floyd gave me, as he was cleaning out his stuff.) Optional.

And... if you want to see something more modern... a few years ago, two 513 students had to miss a few lectures to attend OSDI (the flagship conference for operating systems research). At the same time that we were going over classic Floyd-Hoare software verification, the OSDI folks were getting a talk from some folks at Microsoft (with academic collaborators) on an end-to-end software verification project using Floyd-Hoare reasoning (helped by the sort of automation we'll get to soon). It's a cool paper, and they did some really impressive stuff. At the same time, you can see the weakness of this approach, as there's still a huge amount of manual effort to add the required annotations, which limits scalability and economic viability. I saw Chris give a great talk on a related project (verifying cryptographic code) last summer, and activity in this area is continuing. Chris Hawblitzel, Jon Howell, Jacob Lorch, Arjun Narayan, Bryan Parno, Danfeng Zhang, Brian Zill, "Ironclad Apps: End-to-End Security via Automated Full-System Verification", OSDI 2014. (Optional)

Hooray! Looks like I'll have time to talk about symbolic execution this week, too!

Week 4 (Guest Lectures by Sam Bayless):

Sam has recommended a great survey paper on SMT solving, by two of the very best experts out there. This is much better than the papers I used to use. Leonardo de Moura, and Nikolaj Bjorner, "Satisfiability Modulo Theories: An Appetizer," Formal Methods: Foundations and Applications -- 12th Brazilian Symposium on Formal Methods, Springer LNCS Volume 5902, 2009, pp. 23-36. SMT is basically SAT solving, but with additional logics that are very useful for software verification and other applications where you don't want to model everything as Booleans.

Weeks 5 and 6 (Week 5 was short due to Thanksgiving):

The first lecture was a grab-bag of topics, to help set up the more advanced material, so there's no specific reading.

David L. Dill, Andreas J. Drexler, Alan J. Hu, and C. Han Yang, "Protocol Verification as a Hardware Design Aid", International Conference on Computer Design, 1992. This is a light-weight paper on the value of using very high-level formal verification to debug hardware. It also introduces the Murphi verifier, which is a nice system to play with guarded commands, non-determinism, and reachability.

C. Norris Ip and David L. Dill, "Better Verification Through Symmetry", International Conference on Computer Hardware Description Languages, 1993. This paper describes automatic symmetry reductions for explicit state enumeration -- one of the cool tricks that can greatly reduce the number of states you need to explore. (Optional)

For hash compaction as implemented in Murphi, it looks as if the definitive paper never got published. For a citable reference, try U. Stern and D. L. Dill. Improved Probabilistic Verification by Hash Compaction, Correct Hardware Design and Verification Methods: IFIP WG 10.5 Advanced Research Working Conference, CHARME '95 Springer LNCS Volume 987, 1995, pp. 206-224. For the state-of-the-art using Bloom filters, see Peter C. Dillinger and Panagiotis Manolios, Bloom Filters in Probabilistic Verification, FMCAD 2004. ( All of these papers are optional.)

Symbolic Reachability: I haven't found a description of the basic reachability computation with BDDs that fits into the course well. Accordingly, I list here three optional papers. The simplest description is one I wrote for a survey paper a million years ago. Section II.C is the relevant part. Alan J. Hu, "Formal Hardware Verification with BDDs: An Introduction", IEEE Pacific Rim Conference on Communications, Computers, and Signal Processing (PACRIM'97), 1997. This is a bit too breezy for our course. Two other possible papers are "A Unified Framework for the Formal Verification of Sequential Circuits" by Coudert and Madre, which is a dense, but good paper by two of the pioneers in this area, and "Implicit State Enumeration of Finite State Machines using BDD's [sic]" by Touati, Savoj, Lin, Brayton, and Sangiovanni-Vincentelli, which is easier to read, although I don't particularly like some of their notation. Both of these papers appeared in the International Conference on Computer-Aided Design in 1990. ( All of these papers are optional.)

Week 7:

And now, we get to symbolic model checking. There are actually two different Turing Awards discussed in this week's material.

Week 8

We'll do a compressed module on SAT-based model-checking. I'm going to focus on the two methods (BMC and IC3) that are currently the most important in practice, although pretty much every method out there is still the best in some cases in practice, and it's sometimes very helpful to understand older methods in order to really understand newer ones. Sadly, we don't have enough time to do everything.

A. Biere, A. Cimatti, E. M. Clarke, and Y. Zhu, "Symbolic Model Checking without BDDs," Tools and Algorithms for the Analysis and Construction of Systems (TACAS'99), LNCS Vol. 1579. (link to old, local copy) This is the original paper on bounded model checking.

OK, here are the core IC3 papers:

Sam Bayless, Celina G. Val, Thomas Ball, Holger H. Hoos, Alan J. Hu, "Efficient Modular SAT Solving for IC3", Formal Methods in Computer-Aided Design (FMCAD), 2013, pp. 149-156. This is an amazing paper, by some truly brilliant researchers, which brings together ideas from SAT, SMT, BMC, IC3, interpolation, induction, and probably a few other ideas from the class that I can't think of right now... (Optional) (All joking aside, I really love how this paper ties together a whole bunch of other ideas. However, I can't justify it as a must-read in our limited time.)

Week 9:

For predicate abstraction, I'm going to assign:
Satyaki Das, and David L. Dill, "Successive Approximation of Abstract Transition Relations," Proc. of the Sixteenth Annual IEEE Symposium on Logic in Computer Science (LICS), June 2001. (old link to non-paywalled ps file)
This paper is a compromise assigned reading between the original paper on predicate abstraction (see below) and more recent papers with fancier heuristics. Section 2 is a good review of the idea of (conservative) abstraction in general, and this paper still gets cited quite a bit.

The original paper on predicate abstract:
Susanne Graf, and Hassen Saidi, "Construction of Abstract State Graphs with PVS", Conference on Computer-Aided Verification (CAV), 1997, Springer LNCS 1254. (Optional)
is also a great paper, and if you're interested in the idea, you should take a look as well.

Thomas Ball, Sriram K. Rajamani, "Bebop: A Symbolic Model Checker for Boolean Programs", SPIN 2000 Workshop on Model Checking of Software, LNCS 1885, August/September 2000, pp. 113-130. This paper describes computing reachability over "Boolean programs", which are essentially pushdown automata. This was the original model-checking engine behind Microsoft's SLAM project.

Thomas Ball, Rupak Majumdar, Todd Millstein, Sriram K. Rajamani, "Automatic Predicate Abstraction of C Programs", PLDI 2001, SIGPLAN Notices 36(5), pp. 203-213. This paper describes mapping real C programs to Boolean programs, using predicate abstraction. (Optional) (This paper basically "concretizes" (pun, haha) the connection between the more theoretical work on predicate abstraction and Boolean programs with actual software.)

Week 10:

OK, this is a short week (only 1 lecture) due to Remembrance Day. I know that people voted not spend time on hybrid systems, but I think you should get some exposure to the basics. I'm going to skip most of the details (usually, I'd spend about 2 weeks on this), and then try to condense about 3 lectures worth of material into one day. :-) We'll basically just look at basic concepts and definitions. For your reference, these are a great set of lecture notes to introduce continuous and hybrid systems, developed by John Lygeros of the University of Patras: John Lygeros, "Lecture Notes on Hybrid Systems", Notes for an ENSIETA short course, February 2-6, 2004. . (Optional) (This document appears to be floating around unpublished. Obviously, we don't have time to go through all of this, but these notes are provided as a background reference for you.

In the unlikely event that we have some spare time, Alur-Dill timed automata are a very cool special case of hybrid systems: Rajeev Alur, Costas Courcoubetis, and David Dill, "Model-Checking in Dense Real-Time", Information and Computation, May 1993, pp. 2-34. (Optional)

Don't read ahead of here (unless you want to), since I haven't picked all the papers for this year yet. The "week" labels are also likely very wrong, since the course has been reorganized.

Possibly Later: