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

January 7: Course overview

• Slides
• binary-search.lisp

January 9: Formal Methods in practice

• “Building Certified Concurrent OS Kernels”, R. Gu, Z. Shao, H. Chen, J. Kim, J. Koenig, X. Wu, V. Sjöberg, and D. Costanzo, Communications of the ACM, Vol. 62 No. 10 (Oct. 2019), pages 89-99.
  Mark's paper summary.
• “Data-Driven Formal Reasoning and Their Applications in Safety Analysis of Vehicle Autonomy Features”, C. Fan, B. Qi, S. Mitra, IEEE Design & Test, Vol. 35, No. 3 (May/June 2018), pages 31-38.
  Mark's paper summary.

January 14: SAT solving with DPLL

I like the presentation in the Handbook of Satisfiability, but I can't find an only version. There are many on-line slide-decks and other descriptions of the algorithm including the original paper in the CACM (here's a link to the PDF).

The plan we decided on in class is that you can find any reference you like. You can write a summary (providing a full citation so I can look it up) and it will count towards your paper summary score loke any other write up. Note: you can find two or more sources, but you'll get credit for one summary -- you can't satisfy the entire paper-summary requirement by finding 20 slide-decks on DPLL and writing a “summary”!

• dpll.jl
• example.jl

January 16: SAT solving with CDCL

• Handbook of Model Checking, Chapter 9: “Propositional SAT solving”
• Alternative: “The Quest for Efficient Boolean Satisfiability Solvers”, L. Zhang and S. Malik, in 14th CAV, LNCS Vol. 2404, pages 17-36 (July 2002). Springer.

January 21: SAT solving application

January 23: Distinguished Lecture Series Talk

• Design Problems: Trustworthy Smart Devices and 3D Printed Lace
• Mary Baker, HP Labs
• January 23, 3:30-5pm, Chemical & Biological Engineering (CHBE), Room 101 - 2360 East Mall
• Abstract: A growing number of domestic spaces incorporate products that collect data from cameras, microphones and other sensors, leading to privacy concerns. In this talk I report on two user studies performed to learn about perceptions of privacy and trust for sensor-enabled, connected devices such as smart home assistants. The study results suggest that users are more likely to trust devices with materially representative privacy status indicators. This means that the indicators themselves are part of what determines what sensing can take place. I will describe how we have applied the study results to the design of current devices and what the implications are for the physical design of future smart devices.
• Speaker's Bio: Mary Baker is an architect and senior technologist at HP Inc. in Palo Alto. Her interests cover a broad range of areas where predicting and solving problems tangibly improves the experience people have with technology. Her research topics include mobile systems and applications, physical affordances for IoT privacy, digital preservation, authentication, and design and workflow for additive manufacturing. Before joining HP in 2003 she was on the faculty of the computer science department at Stanford University where she led the MosquitoNet and Mobile People Architecture projects and graduated 7 Ph.D. students. She has received a Sloan Foundation Fellowship, an Okawa Foundation Grant, and an NSF CAREER Award and was designated an ACM Distinguished Engineer. She is a member of the DARPA Information Science and Technology (ISAT) Study Group and is a founding member of the editorial board for IEEE Pervasive Computing, for which she also writes the popular “Notes from the Community” column. She received an A.B. in Mathematics and an M.S. and Ph.D. in Computer Science, all from the University of California at Berkeley.

January 28: Finish up CDCL SAT solving

January 30: Binary Decision Diagrams

• “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)
• An alternative reading is “Binary Decision Diagrams”, R.E. Bryant, Chapter 7 in Handbook of Model Checking, editors: E.M. Clarke, T.A. Henzinger, H. Veith, and R. Bloem.

• “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)

February 4: Intro to Model Checking

• “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)
• Slides

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

February 6: a model-checking example

• “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)
• "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)

February 11: Intro to symbolic execution

• “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)

February 13: a symbolic execution example

Feb. 18, 20: spring break

February 25: intro to SMT

• “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)
• “Simplification by Cooperating Decision Procedures”, G. Nelson, and D.C. Oppen, ACM Transactions on Programming Languages and Systems, Vol. 1, No. 2, pages 245-257, (Oct. 1979).
  

• “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)

Feb. 27:

Mar. 3: SMT and symbolic execution example:

Mar. 5: Resolution

Mar. 10: SMT based model checking

Mar. 12: SMT based model checking

Mar. 17: Theorem proving with ACL2

Mar. 19: More (Moore?) ACL2

• notes.pdf, notes for lecture
• sum.lisp, sum of the first n natural numbers.
• qsort.lisp, quick sort
• perm.lisp, permutations

Mar. 24: Integrating an SMT Solver into ACL2

Mar. 26: More on Smtlink

Mar. 31: Separation logic

Apr. 2: Applications of separation logic

• “Moving Fast with Software Verification”
• Having read the paper, I looked at some of the references. Here's one that I think would have been the “right” paper for today
    “Infer: An Automatic Program Verifier for Memory Safety of C Programs”
  I'll refer to it in the lecture.
• Here's the public canvas link for class visitors.

Apr. 7: Synthesis

• “SpaceInvader” or “SLAyer”,
• “Viper: A Verification Infrastructure for Permission-Based Reasoning Verification, Model Checking, and Abstract Interpretation”
  An it comes with a tutorial.

And beyond...