CpSc 513: Introduction Formal Verification -- Reading List

This list will certainly change as the term progresses. Quite a few of the papers are quite 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.

September 10:

• Course overview (no reading assigned).
• lecture slides
• For further reading:

September 15:

• “Automatic Exploit Generation”, T. Avgerinos, S.K. Cha, A. Rebert, E.J. Schwartz, M. Woo, and D. Brumley. Communications of the ACM, Vol. 57 No. 2, pages 74-84, (Feb. 2014).
  (non-UBC link)

September 17:

• “Satisfiability Modulo Theories: An Appetizer”, L. de Moura, and N. Bjørner, in 12^th Brazilian Symposium on Formal Methods, LNCS Vol. 5902, pages 23-36 (Aug. 2009). Springer. (non-UBC link)
• “Satisfiability Modulo Theories: Introduction and Applications”, L. de Moura, and N. Bjørner, in Communications of the ACM, Vol. 54 No. 9, pages 69-77, (Sep. 2011).
  (non-UBC link)

September 22:

• “Symbolic Execution for Software Testing: Three Decades Later”, C. Cadar and K. Sen, in Communications of the ACM, Vol. 56 No. 2, pages 82-90, (Feb. 2013).
  (non-UBC link)

• “CUTE: a concolic unit testing engine for C”, K. Sen, D. Marinov, and G. Agha, in 10^th ESEC, pages 263-272 (Sep. 2005).
  (non-UBC link)
• “KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs”, C. Cadar, D. Dunbar, and D. Engler, in OSDI'08, pages 209-224 (Dec. 2008).
  (non-UBC link)

September 24:

• “Symbolic execution and program testing”, J. King, in Communications of the ACM, Vol. 19 No. 7, pages 385-394, (July 1976).
  (non-UBC link)

• “An Axiomatic Basis for Computer Programming”, C.A.R. Hoare, in Communications of the ACM, Vol. 12 No. 10, pages 576-580, (Oct. 1969).
  (non-UBC link)
• “Guarded Commands, Non-Determinacy, and Formal Derivation of Programs”, E.W. Dijkstra, in Communications of the ACM, Vol. 19 No. 8, pages 576-580, (Aug. 1976).
  (non-UBC link)

September 29:

• Handbook of Satisfiability ( A. Biere, M. Heule, H. van Maaren, and T. Walsh, Eds), Chapter 3: "Complete Algorithms", A. Darwiche and K. Pipatsrisawat.
  We'll cover Sections 3.5-3.7 which describes the DPLL SAT solving algorithm along with the basic ideas that motivate more advanced algorithms.

• “The Quest for Efficient Boolean Satisfiability Solvers”, L. Zhang and S. Malik, in 14^th CAV, LNCS Vol. 2404, pages 17-36 (July 2002). Springer.
  (non-UBC link)
• “Understanding the empirical hardness of NP-complete problems”, K. Leyton-Brown, H. Hoos, F. Hutter, and Lin Xu, in Communications of the ACM, Vol. 57, No. 5, pages 98-107, (May 2014).
  (non-UBC link)
• “A survey of recent advances in SAT-based formal verification”, M.R. Prasad, A. Biere, A. Gupta, in Software Tools for Technology Transfer, Vol 7, No. 2, pages 156-173 (Apr. 2005), Springer.
  (non-UBC link)

October 1:

• “Symbolic Boolean Manipulation with Ordered Binary-Decision Diagrams”, R.E. Bryant, in ACM Computing Surveys, vol. 24, no. 3, pages 293-318 (Sept. 1992).
  (non-UBC link)

• “Formal hardware verification with BDDs: an introduction”, A.J. Hu, in IEEE Pacific Rim Conference on Communications, Computers and Signal Processing, pages 677-682 (Aug. 1997).
  (non-UBC link)
• “On the complexity of VLSI implementations and graph representations of Boolean functions with application to integer multiplication”, R.E. Bryant, in IEEE Transactions on Computers, Vol. 40, no. 2, pages 205-213 (Feb. 1991).
  (non-UBC link)
• “Equivalence checking using cuts and heaps”, A. Kuehlmann and F. Krohm, in 34^thDesign Automation Conference, pages 263-268 (June 1997).
  (non-UBC link)

October 6:

• “Replacing Testing with Formal Verification in Intel^® Core^TM i7 Processor Execution Engine Validation”, R. Kaivola, R. Ghughal, N. Narasimhan, A. Telfer, J. Whittemore, S. Pandav, A. Slobodová, C. Taylor, V. Frolov, E. Reeber, and A. Naik, in 21^st CAV, LNCS Vol. 5643, pages 414-429 (June 2009). Springer.
  (non-UBC link)

• “Symbolic Trajectory Evaluation: The Primary Validation Vehicle for Next Generation Intel^&ref; Processor Graphics FPU”, M Achutha KiranKumar V, Aarti Gupta, Rajnish Ghughal, in FMCAD'12 (Oct. 2012).
  (non-UBC link)

October 8:

• “Model Checking: Algorithmic Verification and Debugging” (Turing Award Lecture), E.M. Clarke, E.A. Emerson, and J. Sifakis, in Communications of the ACM, Vol. 52 No. 11, pages 74-84, (Nov. 2009).
  (non-UBC link)

• “Symbolic model checking: 10²⁰ states and beyond”, J.R. Burch, E.M. Clarke, K.L. McMillan, and D. Dill, in 5^th LICS, pages 428-439, (June 1990).
• The SMV System (Ph.D. thesis), K.L. McMillan, 1993.

October 13:

• “Automatic verification of the SCI cache coherence protocol”, U. Stern and D. Dill, in CHARME'95 LNCS Vol. 987, pages 21-34 (Oct. 1995). Springer.
  (non-UBC link)

• “Protocol Verification as a Hardware Design Aid”, D. Dill, A.J. Drexler, A.J. Hu, and C.H. Yang, in ICCD'92, pages 522-525 (Oct. 1992).
• “Better verification through symmetry”, C. Norris Ip, D. Dill, in Formal Methods in System Design, Vol. 9, No. 2, pages 41-75 (Aug. 1996).
  (non-UBC link)
• “A Simple Method for Parameterized Verification of Cache Coherence Protocols”, C-T. Chou, P.K. Mannava, S.Park, in 5^{th FMCAD}, LNCS Vol. 3312, pages 382-398 (Nov. 2004), Springer.
  (non-UBC link)
• “A case study in model checking software systems”, J.M. Wing and M. Vaziri-Farahani, in Science of Computer Programming Vol. 28, No. 2-3, pages 273–299,(Apr. 1997) Elsevier.
  (non-UBC link)

October 15:

• “Bebop: A Symbolic Model Checker for Boolean Programs”, T. Ball and S.K. Rajamani, in 7^th International SPIN Workshop, LNCS Vol. 1885, pages 113-130 (Aug. 2000). Springer.
  (non-UBC link)

October 20:

• "A Decade of Software Model Checking with SLAM", T. Ball, V. Levin, and S.K. Rajamani, in Communications of the ACM, Vol. 54 No. 7 (July 2011).
  (non-UBC link)

October 22:

October 27:

October 29:

November 3:

November 5:

November 10:

November 12:

November 17:

November 19:

November 24:

November 26:

December 1:

December 3: