Assigned Readings:

I'm always tweaking the reading list this year, so this list will grow gradually. Also, I'm building on the old reading list, 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...)

Markers for roughly when each reading is likely to be appropriate are only approximate, since what we cover each lecture can change.

Week 0:

I used to have a very simple introductory article, giving an industry perspective on formal verification, but it's very out-of-date. I've been looking for a good replacement, but haven't found the perfect paper. Here are some optional readings:

• E. M. Clarke, and R. P. Kurshan, "Computer-Aided Verification", IEEE Spectrum, Vol. 33, No. 6, 1996, pp. 61-67. This is the out-of-date paper I used to hand out many years ago. Back then, formal verification for hardware was just starting to get traction, but things have improved a lot since then. This link is to a scanned copy on Ed's webpage. The quality isn't as good, but you get all the sidebars written by various people at different companies, formatted as originally intended. This link is to the official on-line version at IEEE Xplore.
• Roope Kaivola, Rajnish Ghughal, Naren Narasimhan, Amber Telfer, Jesse Whittemore, Sudhindra Panday, Anna Slobodova, Christopher Taylor, Vladimir Frolov, Erik Reeber, Armaghan Naik, "Replacing Testing with Formal Verification in Intel Core i7 Processor Execution Engine Validation", Proceedings of 21st International Conference on Computer-Aided Verification (CAV'09), Springer LNCS Vol. 5643, pp. 414-429, 2009. This is much more recent. The paper is long and detailed, but it describes Intel's experience using formal verification instead of traditional simulation-based methods, resulting in lower cost and higher quality. Intel has been investing heavily in formal verification since the Pentium FDIV bug back in 1995.

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 now, although the whole paper is excellent. The above link is to an old Postscript file that displays upside down on many viewers now. (Fixed, thanks to Sam Bayless!) Here is a link to the official version at the ACM Digital Library. You have free access from UBC machines.

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.) Download article if you're on a UBC machine.

Here is additional explanation of the combinatorial part of Bryant's multiplication proof. Optional

Week 2:

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

Vipin Kumar, "Algorithms for Constraint Satisfaction Problems: A Survey", AI Magazine, Volume 13, Number 1, pp. 32-44, 1992. Domagoj Babic pointed me to this survey paper. I don't really like it, because it's very broad, and too AI-ish for this course. However, it is a very broad survey of the general background behind solving constraint satisfaction problems, of which SAT is one instance. You may enjoy reading it as background and landscape behind this very general class of problems. (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. This will be moved to later in the course!

On Thursday, I talked about practical tricks for combinational equivalence checking. These are some of the classic references: (Optional)

• Daniel Brand, "Verification of Large Synthesized Designs", International Conference on Computer-Aided Design, pp. 534-537, 1993. This is probably the most cited paper, presenting a fully worked out version of the cutpoint idea. But, it's old and so harder to read.
• C. Leonard Berman and Louise H. Trevillyan, "Functional Comparison of Logic Designs for VLSI Circuits", International Conference on Computer-Aided Design, pp. 456-459, 1989. This is the original introduction of the cutpoint idea, but this paper is even older and harder to read.
• Andreas Kuehlmann and Florian Krohm, "Equivalence Checking Using Cuts and Heaps", 34th Design Automation Conference, pp. 263-268, 1997. This papers covers most of the tricks used in modern tools.

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.

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 a hardcopy reprint and can make copies if anyone is interested. Optional.

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. Optional.

For symbolic simulation of software, here are two invited papers in the International Journal of Parallel Programming. UBC's library has electronic access to these.

• Alfred Koelbl and Carl Pixley, "Constructing Efficient Formal Models from High-Level Descriptions Using Symbolic Simulation", International Journal of Parallel Programming, 33(6), December 2005, pp. 645-666. This paper focuses on the symbolic execution, with nice figures and all, which is what I want, but they are at the bit-level. Focus on the basic ideas and don't worry abou the details (in particular, don't worry too much about loops, recursion, and pointers yet).
• David Currie, Xiushan Feng, Masahiro Fujita, Alan J. Hu, Mark Kwan, and Sreeranga Rajan, "Embedded Software Verification Using Symbolic Execution and Uninterpreted Functions," International Journal of Parallel Programming, 34(1), January 2006, pp. 61-91. This paper, by an amazing set of authors, does the symbolic simulation using uninterpreted functions, which is a handy abstraction that we'll cover soon, but it's on assembly language programs, and most of the paper is about the details to get the idea to work on real examples. Optional.
• Oh, just for fun, here's another optional paper, where we see the cutpoint idea reappearing for checking equivalence of software: Xiushan Feng, and Alan J. Hu, "Cutpoints for Formal Equivalence Verification of Embedded Software", International Conference on Embedded Software (EMSOFT), 2005, pp. 307-316. Optional.
• If you want to see how far SAT and symbolic execution can get you, check this paper out: Domagoj Babic and Alan J. Hu, "Calysto: Scalable and Precise Extended Static Checking", 30th International Conference on Software Engineering (ICSE'08), 2008, pp. 211-220. A lot of this paper will make more sense to you later in the course. Optional.

Week 4:

I'm still looking for the perfect intro paper on decision procedures for the variety of theories used in software verification. (This now goes under name "Satisfiability Modulo Theories", which I don't like, but it's become standard.) I've selected two readings I like. Please read at least one of these, and I'll be interested in hearing how it went:

• Greg Nelson, and Derek C. Oppen, "Simplification by Cooperating Decision Procedures," ACM Transactions on Programming Languages and Systems, 1(2), October 1979, pp. 245-257. This is a classic paper on the topic. Nelson and Oppen pioneered this area, and their work still underlies and guides a lot of research in this area.
• Leonardo de Moura, Slides from Invited Tutorial on SMT Solvers, Formal Methods in Computer-Aided Design, 2006. These are a great set of slides prepared by Leonardo de Moura, who is one of the top experts working in this field now. They are up-to-date and very comprehensive. I remember being amazed by them when I saw this tutorial, and many people I know consider this the best source to learn about this area. However, they are slides, so it's very tough to just read by youself. These also go way beyond what we need for this course. BTW, if you want to print these, you'll probably want to use psnup or similar commands to print multiple slides on one page.
• Roberto Bruttomesso, Alessandro Cimatti, Anders Franzen, Alberto Griggio, and Roberto Sebastiani, "Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: A Comparative Analysis", Annals of Mathematics and Artificial Intelligence, Vol. 55, No. 1-2, pp. 63-99. I think this paper is my current favorite, although it's kind of long and dense. It covers a newer approach than Nelson-Oppen, but the basic introductory material is good, too.

Here is a write-up of the example in class, worked in full, of the communicating decision procedures.

Week 5:

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, it looks as if the definitive paper hasn't gotten published yet. I believe the definitive treatment is this manuscript: P. Wolper, U. Stern, D. Leroy, and D. L. Dill, Reliable Probabilistic Verification Using Hash Compaction For a citable reference, try U. Stern and D. L. Dill. A New Scheme for Memory-Efficient Probabilistic Verification, Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols, and Protocol Specification, Testing, and Verification, pages 333-48, 1996. For the newer, better work using Bloom filters, see Peter C. Dillinger and Panagiotis Manolios, Bloom Filters in Probabilistic Verification, FMCAD 2004. ( All of these papers are optional.)

Week 6:

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

For temporal logic, E. Allen Emerson has written an amazing chapter in the Handbook of Theoretical Computer Science. This book is well worth buying. But, a draft of the chapter is available on-line directly from Allen. This is optional. It's an encyclopedic reference.

J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang, "Symbolic Model Checking: 10^{20} States and Beyond", Information and Computation, Vol. 98, No. 2, June 1992. This is the journal version of the original paper on symbolic model checking (which appeared in the Conference on Logic in Computer Science in 1990). The paper goes into more depth than what I expect of you and is rather theoretical, but I want you all to understand symbolic model checking for CTL at least. (We'll cover roughly the material from Sections 1-4 and 6 in class.)

Week 8:

This is background material for Ian Mitchell's lectures. We'll use a set of lecture notes 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. . (This document appears to be floating around unpublished. Here is another link if the above is broken. Obviously, we don't have time to go through all of this, but these notes are provided as a background reference for you.

This paper is for Ian's lecture on November 3. Ian M. Mitchell, "Comparing Forward & Backward Reachability as Tools for Safety Analysis" in Hybrid Systems Computation and Control (Alberto Bemporad, Antonio Bicchi, and Giorgio Buttazzo eds.), LNCS 4416, pp. 428-443 (2007). And here is an older version of slides for his lecture.

Week 9:

This paper is for Ian's lecture on November 8. Claire J. Tomlin, Ian M. Mitchell, Alexandre M. Bayen, and Meeko Oishi, "Computational Techniques for the Verification of Hybrid Systems" in Proceedings of the IEEE, volume 91, number 7, pp. 986-1001 (July 2003). And here is the current version of slides for his lecture.

Here are an old version of the slides for Ian's lecture on November 10. For reading, you can look at Chao Yan's homepage for the Coho work done at UBC, and also Goran Frehse, Colas Le Guernic, Alexandre Donze, Scott Cotton, Ray Rajarshi, Olivier Lebeltel, Rodolfo Ripado, Antoine Girard, Thao Dang, and Oded Maler, "SpaceEx: Scalable Verification of Hybrid Systems", International Conference on Computer-Aided Verification (CAV 2011), Springer LNCS 6806, 2011, pp. 379-395.

Week 10:

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.
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.

I'm delighted to see MIT has put an entire course on abstract interpretation on-line, taught by Patrick Cousot himself. There's more reading here than you could ever want on abstract interpretation (all of this is optional). Cousot is listing Patrick Cousot, "Abstract Interpretation Based Formal Methods and Future Challenges," Informatics, 10 Years Back -- 10 Years Ahead, Springer LNCS 2000, pp. 138-156, 2001. as the introductory paper on abstract interpretation. I skimmed it, and it looks easier than the original 1977 POPL paper by Patrick and Radhia Cousot which is definitely worth a read, too. BTW, it's funny to see that the final exam is to prove that model checking is just an abstract interpretation.

For basic static program analysis, Michael Schwartzbach from BRICS in Denmark has written a great set of lecture notes. Strangely, the link from his page goes to an internal webserver with an invalid security certificate, but here's another link . This is optional, but it's a great background reference for what we'll talk about on Thursday.

Week 11:

On Tuesday, we finished the static analysis stuff from last week. During lecture, I mentioned the chicken chicken chicken talk, and this is the more serious article (on the importance of giving good talks, by Moshe Vardi, who is very active in the formal verification world in addition to being editor of CACM) where I saw the reference to the aforementioned talk. (The preceding are obviously not assigned readings, but just for fun.)

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. This is the original paper on bounded model checking.

K. L. McMillan, "Interpolation and SAT-Based Model Checking," Computer-Aided Verification: 15th International Conference (CAV'2003), LNCS Vol. 2725, Springer, 2003, pp. 1-13. This paper was a major breakthrough on using interpolation for model checking. It was the "coolest" paper on using SAT for model checking until the IC3 stuff came on the scene just recently.

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 also a nice time to re-visit this paper, which I had listed many weeks back when we were working on SAT, as the interpolants that Ken usees are derived from the resolution proof. (Optional)

Week 12:

OK, here are the core IC3 papers:

• Aaron R. Bradley, "SAT-Based Model Checking Without Unrolling," Verification, Model Checking, and Abstract Interpretation (VMCAI), 2011. This paper is considered the authoritative reference for IC3. In hindsight, I think this paper is really the must-read if you want to understand IC3. The next two papers are friendlier, but they aren't precise enough to understand the details. You might start with those, though.
• Fabio Somenzi, and Aaron R. Bradley, "IC3: Where Monolithic and Incremental Meet", Formal Methods in Computer-Aided Design (FMCAD) 2011. This is meant as a gentle tutorial, and it includes a fully worked small example.
• "Efficient Implementation of Property Directed Reachability", Formal Methods in Computer-Aided Design (FMCAD) 2011. This paper is also meant to be explanatory, as well as going into optimizations from the PDR folks. I found this easier to follow overall, but there were spots that were hard to pin down.
• Aaron Bradley, and Zohar Manna, "Checking Safety by Inductive Generalization of Counterexamples to Induction", Formal Methods in Computer-Aided Design (FMCAD), 2007, pp. 173-180. This is the origin of the idea, but it's not the newest version of IC3. It does contain more info on clause generalization, though. It's also interesting for historical reference.

Possibly Later:

For Zvonimir's talk on Monday, if you want background reading, you can take a look at some of his papers (All optional):

• Shuvendu Lahiri, Shaz Qadeer, Zvonimir Rakamaric, "Static and Precise Detection of Concurrency Errors in Systems Code Using SMT Solvers", 21st International Conference on Computer Aided Verification (CAV 2009), Grenoble, France
• Zvonimir Rakamaric, Alan J. Hu, "A Scalable Memory Model for Low-Level Code", 10th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI 2009), Savannah, GA, USA
• Zvonimir Rakamaric, Alan J. Hu, "Automatic Inference of Frame Axioms Using Static Analysis", 23rd IEEE/ACM International Conference on Automated Software Engineering (ASE 2008), L'Aquila, Italy

For Flavio's talk on Wednesday, the best publicly available reference is Flavio M. De Paula, Marcel Gort, Alan J. Hu, Steven J. E. Wilton, and Jin Yang, "BackSpace: Formal Analysis for Post-Silicon Debug", International Conference on Formal Methods in Computer-Aided Design (FMCAD), 2008, pp. 35-44. (Optional)

Week 10:

I haven't found papers on abstraction that would fit particularly well for the course yet.

Week 11:

Week 12: