Department of Computer Science
CPSC 513: Integrated System Design

Assigned Readings:

By popular request, I am putting in markers for roughly when each reading is likely to be appropriate. Note that these are only approximate, since what we cover each lecture can change.

Week 1 and 2:

Edmund M. Clarke and Robert P. Kurshan, "Computer-Aided Verification", IEEE Spectrum, June 1996, pp. 61-67. This article is getting a bit dated, but it's a quick read, with minimal technical content, describing the field. The sidebars are an excellent snapshot of the work that's happening in industry. Download article if you're on a UBC machine. Or get a hardcopy from me.

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.

Henrik Reif Andersen, "An Introduction to Binary Decision Diagrams". Matt Pedersen and Jesper Moeller pointed me to these notes which were used to introduce BDDs at the Technical University of Denmark and the IT University in Denmark. You might prefer them to Randy Bryant's survey paper. (Optional.)

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

Week 3:

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

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

Week 4:

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.

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.

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. ( Both of these papers are optional.)

Week 5:

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. Ask me if you'd like a copy of the ones that aren't on-line. 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 6:

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

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 modern, complete SAT solvers for verification applications.

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

Week 7:

John C. Mitchell, Mark Mitchell, and Ulrich Stern, "Automated Analysis of Cryptographic Protocols Using Murphi", IEEE Symposium on Security and Privacy, 1997, pp. 141-151. This paper is one of the first to apply model-checking techniques to security protocols.

Gavin Lowe, "Breaking and Fixing the Needham-Schroeder Public-Key Protocol using FDR", In Tools and Algorithms for the Construction and Analysis of Systems, Margaria and Steffen (eds.), volume 1055 of Lecture Notes in Computer Science, Springer Verlag, pages 147-166, 1996. Also in Software Concepts and Tools, 17:93-102, 1996. This is the breakthrough paper that inspired the one above. It's a bit longer and more specialized, so I've given the Mitchell-Mitchell-Stern paper as the required reading, with this as background for people who are interested in going to the source. Optional

D. Song, S. Berezin, and A. Perrig, "Athena, a Novel Approach to Efficient Automatic Security Protocol Analysis", Journal of Computer Security, Vol. 9, Nos. 1 and 2, 2001, pp. 47-74. This is something much more recent, plus two of the three authors were interviewing for faculty jobs here before. Optional

Week 8:

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. ? (to appear), Springer-Verlag, 2000. I've been browsing for a good survey paper on probabilistic verification. I haven't found a survey, but this paper comes close -- it's recent, provides an overview, and has numerous citations if anyone wants to pursue this area further.

A. Bianco and L. de Alfaro, "Model Checking of Probabilistic and Nondeterministic Systems" Foundations of Software Technology and Theoretical Computer Science, Lecture Notes in Computer Science 1026, pages 499-513, Springer-Verlag, 1995. This is an earlier paper that provides some more details on the basic ideas. (Optional)

Week 9:

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.

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.

Week 10:

Dawson Engler and Madanlal Musuvathi, Static analysis versus software model checking for bug finding, invited paper at VMCAI 2004. This is the high-level overview paper on a string of work from these guys. You should check out Dawson Engler's home page for more detailed papers on each project.

The following papers are not assigned this year:

Jerry R. Burch and David L. Dill, "Automatic Verification of Pipelined Microprocessor Control", International Conference on Computer-Aided Verification, 1994. This paper was a big step forward in automatic formal verification for pipelined microprocessors. This continues to be an active area of research (industrial and academic).

Xiushan Feng and Alan J. Hu, ``Automatic Formal Verification for Scheduled VLIW Code,'' ACM SIGPLAN Joint Conference: Languages, Compilers, and Tools for Embedded Systems, and Software and Compilers for Embedded Systems, pp. 85-92, ACM Press, 2002. This paper is essentially using the exact same ideas from the Burch-Dill paper (symbolic execution with uninterpreted functions) to do software verification of low-level code for messy processors. Opetional

George C. Necula and Peter Lee, "Safe Kernel Extensions Without Run-Time Checking", Symposium on Operating System Design and Implementation, 1996. This paper describes how to send a proof of correctness along with code, so that untrusted code can be executed safely.

Rajeev Alur, Costas Courcoubetis, and David Dill, "Model-Checking in Dense Real-Time", Information and Computation, May 1993, pp. 2-34. This paper describes how to extend model-checking to deal with timing constraints. The conference version of this paper was a breakthrough that sparked considerable further research.

Eric C. R. Hehner, "A Practical Theory of Programming", Science of Computer Programming, vol. 14, 1990, pp. 133-158.

E. C. R. Hehner, "Abstractions of Time", Chapter 12 in A Classical Mind, A. W. Roscoe, Ed., Prentice-Hall International Series in Computer Science, London, 1994, pp. 191-210. For people interested in synthesizing hardware, either T. S. Norvell, "SMALL: A Programming Language for State Machine Design", Canadian Conference on Electrical and Computer Engineering, 1997. or E. C. R. Hehner and T. S. Norvell, "program2circuit", WSES/IEEE World Multiconference on Circuits, Systems, Communications, and Computers, 2001.

Matt Kaufmann, Andrew Martin, and Carl Pixley, "Design Constraints in Symbolic Model Checking", 10th International Conference on Computer-Aided Verification (CAV'98), LNCS Vol. 1427, 1998, pp. 477-487. This is a recent paper (presented here at UBC summer 1998, and Andy Martin is a recent UBC PhD) describing a modification of CTL model checking that gives a better way to model the environment of the system being verified.

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.

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 paper goes with Holger's guest lecture. Bounded model checking allows using a SAT solver to do model checking of bounded temporal properties. This is the original paper on bounded model checking.

Ahmed Bouajjani, Bengt Jonsson, Marcus Nilsson, and Tayssir Touili, "Regular Model Checking", 12th International Conference on Computer-Aided Verification (CAV2000), LNCS Vol. 1855, 2000, pp. 403-418. This is a recent paper that provides a good picture of the state-of-the-art of model checking systems with discrete, unbounded state spaces (e.g., unbounded queues, linear arrays of components, etc.). It also has a lot of references, if you eventually get interested in this area.

Jesper Moeller, Jakob Lichtenberg, Henrik R. Andersen, and Henrik Hulgaard, "Difference Decision Diagrams", Conference of the European Association for Computer Science Logic, September 1999. and Jesper Møller, Jakob Lichtenberg, Henrik R. Andersen, and Henrik Hulgaard, "Fully Symbolic Model Checking of Timed Systems Using Difference Decision Diagrams", Workshop on Symbolic Model Checking, Federated Logic Conference (FLoC), July 1999. These two papers are for Jesper Moeller's guest lecture on November 4. They describe a new data structure, invented by Jesper, and it's application to doing real-time model checking. (Optional)

David Cyrluk, Patrick Lincoln, and Natarajan Shankar, "On Shostak's Decision Procedure for Combinations of Theories", Conference on Automated Deduction (CADE '96), Springer Verlag LNAI 1104, pp 463-477, July 1996. This paper comes highly recommended as an excellent paper on automated deduction procedures.

Andrew C. Myers and Barbara Liskov, "A Decentralized Model for Information Flow Control", 16th Symposium on Operating Systems Principles, 1997. This paper is for Mike Feeley's guest lecture on Thursday, November 5. The abstract is:

This paper presents a new model for controlling information flow in systems with mutual distrust and decentralized authority. The model allows users to share information with distrusted code (e.g., downloaded applets), yet still control how that code disseminates the shared information to others. The model improves on existing multilevel security models by allowing users to declassify information in a decentralized way, and by improving support for fine-grained data sharing. The paper also shows how static program analysis can be used to certify proper information flows in this model and to avoid most run-time information flow checks.
The paper is available in html, postscript, or pdf.

Richard J. Anderson, Paul Beame, Steve Burns, William Chan, Francesmary Modugno, David Notkin, Jon D. Reese, "Model Checking Large Software Specifications", Symposium on the Foundations of Software Engineering, 1996. This is a recent paper on using model checking for software (specification) verification. Gail Murphy will give the talk.