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!
Hey, there's video now, too!
describing current work happening at Amazon Web Services using the sorts of highly automated formal methods that we will be studying. (Note that I attended and enjoyed the talk at FloC, but I haven't watched the entire video, so I can't vouch for the production values.) And if you don't want to watch the video, here's the accompanying paper: although you'll miss little details, like Byron reminiscing that his first conference ever was the 10th CAV that I chaired (with Moshe Vardi) here at UBC in 1998, or the passing mention to MonoSAT, which we developed recently here. (This is optional, too.) (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:
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.
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. For reference, 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. (Optional)
Week 5 (short due to Thanksgiving):
We now shift our focus to "reactive systems", which are systems that maintain an on-going interaction with the environment (cf. "agents"). The key difference is that we now worry about how a system behaves over time, versus just checking whether a function computes the correct result.
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 (Guest Lectures by Sam Bayless):
I'm really happy to have my postdoc and former PhD student Sam Bayless guest-lecturing on these topics, as he's among the best in the world on them.
We'll do a compressed module on SAT-based model-checking. We'll focus on the two methods (BMC and IC3) that are currently the most important in practice, but Sam likes to present this material including some "in-between" methods like k-induction and interpolation.
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.
Here are the core IC3 papers:
For a survey of the pre-IC3 approaches to using SAT for unbounded model checking, Sam recommends Mukul R. Prasad, Armin Biere, and Aarti Gupta, "A Survey of Recent Advances in SAT-Based Formal Verification", Software Tools for Technology Transfer, Vol 7 No 2 (April 2005), pp. 156-173.
And Ken McMillan's original interpolation paper was a major breakthrough and is still a very insightful approach. 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. (Optional)
Week 9 (Guest Lectures by Mark Greenstreet, Itrat Akhter, and Carl Kwan):
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.
(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, which has evolved into production use in Microsoft's Static Driver Verifier.
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 11:
At FMCAD, I was reminded that LTL has becoming increasingly fashionable lately (whereas I have historically emphasized CTL model checking because CTL and model checking go together so well). Therefore, given that many of you may encounter LTL in your research, I figured that I really should give you all an introduction to LTL model checking. I struggled quite a bit to select readings, as there's a vast literature on this topic, some of it quite theoretical. I'm going to select just two papers for you: one to give a taste for the classical, original approach to LTL model checking; and the second to describe one of the main workhorses in practice for checking liveness properties (which tend to get emphasized more in LTL model checking, but also apply for CTL).
Week 12: TBD
Vaastav asked for some coverage of formal verification of
probabilistic systems. This paper is a good introduction:
L. de Alfaro, M. Kwiatkowska, G. Norman, D. Parker, and R. Segala,
"Symbolic Model Checking of Concurrent Probabilistic Processes Using MTBDDs
and the Kronecker Representation",
6th International Worskshop on Tools and Algorithms for the Construction
and Analysis of Systems (TACAS 2000)
LNCS Vol. 1785.
This is also a good chance to introduce influential work that came
directly out of a CPSC 513 project. Robert St. Aubin and Jesse Hoey
were in 513, and this work started as their course project and
became the fastest stochastic planner available. Stochastic planning
is a closely related problem to verification of probabilistic systems.
Jesse Hoey, Robert St. Aubin, Alan Hu, Craig Boutilier,
"SPUDD: Stochastic Planning Using Decision Diagrams",
15th Conference on Uncertainty in Artificial Intelligence (UAI'99),
pp. 279-288.
For Thursday, I figure you should get a brief intro to hybrid systems. I'd normally spend 2 weeks on this material, so we'll just look at the 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.
Week 13: Project Presentations!
We'll have signups for your project presentations on November 27 and November 29. We'll schedule people on 15-minute intervals, so aim for about 10-12 minutes per project (individual or group).
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 mutates a bit every year.
Week 8
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 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)
Possibly Later: