CpSc 538G: Formal Verification and Analysis -- Reading List
This list will certainly change as the term progresses.
My approach is to start topics with papers that were aimed at a general, computer science, audience,
and then follow up with deeper papers from the research literature.
Some of the research papers are 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.
I've borrowed extensively from the excellent
reading list
that
Alan Hu created for earlier offerings of
this course. Feel free to check out
the original.
Alan has some insightful commentary, and he lists some papers that aren't on this list --
in case your looking for something in a category that I've missed.
Welcome to Formal Methods for Analysis and Verification
September 6:
September 7:
SMT is cool, and we can use it to find bugs.
September 12:
- “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)
- lecture notes
- my example of a summary for this paper
September 14:
Choose one of the two papers below to read (and write a short review):
- “Satisfiability Modulo Theories: An Appetizer”,
L. de Moura, and
N. Bjørner, in
12th 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)
- lecture notes
SAT solving: methods and applications
September 19: The DPLL algorithm
For further reading (optional):
- “A machine program for theorem-proving”
M. Davis,
G. Logemann,
D. Loveland, in
Communications of the ACM,
Vol. 57,
- “Boolean Satisfiability: Theory and Engineering”
M. Vardi, in
Communications of the ACM,
Vol. 5,
No. 7, page 394-397, (July 1962).
(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)
September 21: Binary Decision Diagrams
For further reading (optional):
- “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
34thDesign Automation Conference,
pages 263-268 (June 1997).
(non-UBC link)
Carl Seger's Guest Lecture
September 26 & 28: Efficient SAT Solvers
For further reading (optional):
Model Checking
October 3:
For further reading (optional):
- “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
5th 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 5:
For further reading (optional):
October 12 & 17:
October 19:
SMT Solvers
October 24:
For further reading (optional):
- "Simplification by Cooperating Decision Procedures",
G. Nelson, D.C. Oppen, in
ACM Transactions on Programming Languages and Systems (TOPLAS),
Vol. 1, No. 2 (October 1979).
(non-UBC link)
- "Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: A Comparative Analysis",
R. Bruttomesso, A. Cimatti, et al., in
13thInternational Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR),
pages 527-541 (November 2006).
(non-UBC link)
Symbolic software execution
October 26:
For further reading (optional):
- “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)
October 31:
For further reading (optional):
- “CUTE:
a concolic unit testing engine for C”,
K. Sen,
D. Marinov, and
G. Agha, in
10th 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)
November 2:
Interpolation
November 7:
November 9:
IC3
For further reading (optional):
- “SAT-Based Model Checking without Unrolling”,
A. R. Bradley, in
Verification, Model Checking, and Abstract Interpretation (VMCAI),
pages 70-81 (January 2011).
(non-UBC link)
- “Efficient modular SAT solving for IC3”,
S. Bayless, C. G. Val, T. Ball, et al., in
Formal Methods in Computer Aided Design (FMCAD),
(October 2013).
(non-UBC link)
November 14:
Theorem Proving
For further reading (optional):
November 16:
Machine Learning
November 21:
November 23:
- TBD: “The symbiosis of machine learning, symbolic computation, and formal methods”
I. Laradji, M. Schmidt, M. Greenstreet. Work in progress.
Cyber-Physical Systems
November 28 & 30:
- “Designing AI Systems that Obey Our Laws and Values”,
Amitai Etzioni and
Oren Etzioni in
Communications of the ACM,
Vol. 59
No. 9, pages 29-31, (September 2016).
(non-UBC link)
- “Computational techniques for the verification of hybrid systems”,
C. J. Tomlin,
I. M. Mitchell,
A. M. Bayen, and
M. M. K. Oishi, in
Proceedings of the IEEE,
Vol. 91, No. 7,
pages 986-1001 (July 2003).
The first paper sets the stage for some of the important reasons why we should care about cyber-physical systems.
The second paper is much more technical -- it both shows how verification can be applied to a real-world control system,
and it shows (although, not necessarily obviously), how the AI monitors of the first paper might be
included in a real controller.
Beyond this reading list
My goal in teaching CPSC 538G is to provide an introduction and overview of formal methods.
There is much more to the field than can be covered in one term.
Fortunately, we may be able to cover a bit more than the topics on the list above.
Each student in the course is expected to present a paper. You can
- Pick a paper on any topic related to formal methods -- send me a link, and I'll confirm it's suitability.
- Pick a paper on the “For further reading” lists above. There are a few that are
short blog entries, but the rest are acceptable. Again, send me e-mail to claim a paper, and I'll confirm.
- Here are some topics that I wish we had time to cover, but probably won't.
Any of these will be great choices:
- “SLAM2: static driver verification with under 4% false alarms”, T. Ball, E. Bounimova, R. Kumar, V. Levin.
- “Replacing
Testing with Formal Verification in Intel® CoreTM 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
21st CAV,
LNCS
Vol. 5643, pages 414-429 (June 2009).
(non-UBC link)
- “Ironclad Apps: End-to-End Security via Automated Full-System Verification”
C. Hawblitzel, J. Howell et al..
- “Proving program termination”
B. Cook, A. Podelski, A. Rybalchenko.
- “Automating String Processing in Spreadsheets Using Input-Output Examples”
S. Gulwani.
This paper describes the use of SMT techniques in
Flash Fill for Excel.
- “You assume, we guarantee: Methodology and case studies”
T. Henzinger, S. Qadeer, and S. K. Rajamani.
- “Engineering a Static Verification Tool for GPU Kernels”,
E. Bardsley, A. Betts, et al..
- “Qualitative networks: a symbolic approach to analyze biological signaling networks”,
M. A. Schaub, T. A Henzinger, and J. Fisher.
Last modified
(GMT)