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 example 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.
Formal verification is progressing very rapidly right now, and there's
no way we'll cover the whole field in one term. To help make up for
some of the inevitable gaps, I'll move papers that we don't cover in
class to a list of papers "For Further Reading" at the end of this page.
January 2:
January 7:
- "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.
- "Replacing Testing with Formal Verification in Intel Core i7 Processor Execution Engine Validation",
R. Kaivola, R. Ghughal, et al., in
Proceedings of the 21st International Conference on
Computer Aided Verification
(CAV 2009)
- lecture notes
January 9:
"Symbolic Boolean Manipulation with Ordered Binary-Decision Diagrams",
R.E. Bryant, in
ACM Computing Surveys,
vol. 24, no. 3, Sept. 1992.
lecture notes
January 14:
"Equivalence Checking Using Cuts and Heaps",
A. Kuehlmann and F. Krohm, in
Proceedings of 34th Design Automation Conference
(DAC 1997).
January 16:
"Embedded Software Verification Using Symbolic Execution and Uninterpretted Functions",
D. Currie, X. Feng, et al, in
International Journal of Parallel Programming,
vol. 34, no. 1, Feb. 2006.
January 21:
"An Axiomatic Basis for Computer Programming",
C.A.R. Hoare, in Communications of the ACM, vol. 12, no. 10, Oct. 1969.
January 23:
"Guarded Commands, Non-Determinacy, and Formal Derivation of Programs",
E.W. Dijkstra, in Communications of the ACM,
vol. 18, no. 8, Aug. 1975.
January 28 & 30:
"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, Nov. 2009
- Optional: "Protocol Verification as a Hardware Design Aid",
D.L. Dill, A.J. Drexler, et al, in
Proceedings of the 1992 Conference on Computer Design
(ICCD 1992).
February 4:
"The Quest for Efficient Boolean Satisfiability Solvers",
L. Zhang and S. Malik, in
Proceedings of the 14th International Conference on
Computer Aided Verification (CAV 2002).
February 6:
"Satisfiability Modulo Theories: Introduction and Applications",
L. De Moura and N. Bjørner, in
Communications of the ACM, vol. 54, no. 9, Sept. 2011.
February 13:
FAC talk --
slides.
February & 20: Break week
February 25:
"Simplification by Cooperating Decision Procedures",
G. Nelson and D.C. Oppen, in
ACM Transactions on Programming Languages and Systems, Oct. 1979.
February 27:
"Delayed Theory Combination vs. Nelson-Oppen for Satisfiability
Modulo Theories",
R. Bruttomesso, A. Cimatti, et al, in
Annals of Mathematics and Artificial Intelligence,
vol. 55, no. 1-2, Feb. 2009.
March 4:
"Z3: An efficient SMT solver",
L. de Moura and N. Bjørner, in
Proceedings of the 14th International Conference on
Tools and Algorithms for the Construction and Analysis of Systems
(TACAS 2008).
Topics to be covered after the break:
Abstraction:
Kern, Ono-Tesfaye, and Greenstreet,
"A light-weight framework for hardware verification,"
Software Tools for Technology Transfer, vol. 3, no. 3, Aug. 2001
Das and Dill:
"Successive Approximation of Abstract Transition Relations",
LICS 2001
Formal verification of software:
Chatterjee, Lahiri, et al:
"A reachability predicate for analyzing low-level software",
TACAS 2007
Ball, Hackett et al:
"Towards scalable modular checking of user-defined properties",
VSTTE 2010
Cook, Podelski, and Rybalchenko,
"Proving Program Termination",
Communications of the ACM, May 2011
Hybrid systems, robots, automated vehicles:
Tomlin, Mitchell, et al.:
"Computational Techniques for the Verification of Hybrid Systems"
Proceedings of the IEEE, vol. 91, no. 7, July 2003.
Frehse, Le Guernic, et al.:
"SpaceEx: Scalable Verification of Hybrid Systems",
CAV 2011
Eggers, Fränzle and Herde:
SAT Modulo ODE: A Direct SAT Approach to Hybrid Systems
ATVA 2008
Interval arithmetic:
Rump:
"Verification methods: Rigorous results using floating point arithmetic",
Acta Numerica, 2010
Circuits:
Kim, Jeeradit, et al.:
"Leveraging designer's intent: A path toward simpler analog CAD tools",
CICC 2009
Last modified
(GMT)