Some Formal Methods Papers of Interest to the UT ACL2 Seminar
Thank you to all who have contributed these references to papers in formal
methods (and accompanying descriptions), many of which are classic or are
survey papers. Additional contributions are most welcome!
Note: If you can find or improve URLs for
any of these, or (more generally) if you find any missing reference information,
please send email to Matt Kaufmann.
 TPHOLs 2008 has links to tutorial talks on five
major theorem proving systems.
 Benjamin C. Pierce, Types and Programming Languages, has been
highly recommended as a clear introduction to the sorts of type theories
that form foundations for higherorder logic theorem proving systems.
 Edmund Clarke, Armin Biere, Richard Raimi, and Yunshan Zhu.
"Bounded
Model Checking Using Satisfiability Solving". 2001.
 Here are two classic modelchecking papers that could be read together.
The first is Clarke and Emerson's original article that introduced model checking.
The second is about the theory of application of model checking for
finite state system verification.
 Edmund M. Clarke and E. Allen Emerson, "Design and Synthesis of
Synchronization Skeletons Using BranchingTime Temporal Logic", In
D. Kozen (Ed.) Logic of Programs, volume 131 of LNCS, pages 5271,
1981. Springer.
 Edmund M. Clarke, E. Allen Emerson, and A. Prasad Sistla,
"Automatic Verification of Finite State Concurrent Systems Using
Temporal Logic Specifications".
ACM Transactions on Programming Languages and Systems (TOPLAS) archive
Volume 8, Issue 2 (April 1986), pages 244263. ACM, New York, NY,
USA. [ACM Portal with link to pdf file.]
 Edsger W. Dijkstra, "Guarded commands,
nondeterminacy and formal derivation of programs". Communications of the
ACM, 18(8):453457, August 1975.
 Robert Floyd. "Assigning Meanings to Programs", in Proceedings of
Symposium on Applied Mathematics, Vol. 19, J.T. Schwartz (Ed.),
A.M.S., 1967, pp. 1932.
 Susanne Graf and Hassein Saidi. "Construction of abstract state
graphs with PVS". In Proceedings of the 9th Conference on
ComputerAided Verification (CAV'97), Haifa, Israel, June 1997.
Note 1:John Erickson might present the above paper in the seminar.
Note 2:Some software tools, in particular SLAM and BLAST, use predicate
abstraction. Here are references for those:
 SLAM (see also Tom Ball's
web page):
Thomas Ball, Rupak Majumdar, Todd D. Millstein, Sriram K. Rajamani.
Automatic Predicate Abstraction of C Programs PLDI 2001: 203213.
 BLAST:
Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Gregoire Sutre.
"Lazy Abstraction". POPL 2002 : 29th ACM Symposium on Principles of
Programming Languages.
 John Harrison. "Metatheory and Reflection in Theorem Proving: A
Survey and Critique". Technical Report CRC053, SRI International
Cambridge Computer Science Research Center. 1995.
 C. A. R. Hoare. "An
axiomatic basis for computer programming". Communications of the ACM,
12(10):576580, October 1969.
 The following two papers might be read together. The first is about
McCune's prover Otter, and the second is about a later prover of his, EQP. The
second is available online from the UT library web site.
 William McCune. "33 basic test problems: A practical evaluation of
some paramodulation strategies". In Robert Veroff, editor, Automated
Reasoning and its Applications: Essays in Honor of Larry Wos,
chapter 5, pages 71114. MIT Press, 1997.
 William McCune. "Solution of the Robbins problem". Journal of
Automated Reasoning, volume 19(3) pages 263276, 1997.
 Susan Owicki and David Gries. "Verifying Properties of Parallel
Programs: An Axiomatic Approach", Communications of the ACM volume
19(5), pages 279285, 1976.
Note: Owicki has two other papers extending the formalism discussed in
the above paper. If someone is reading the above, perhaps it should
be read together with these others. These are the following:
 Susan Owicki and David Gries. An Axiomatic Proof Technique for
Parallel Programs. Acta Informatica, volume 6, pages 319340,
1976.
 Susan Owicki. A Consistent and Complete Deductive System for
Parallel Programs. ACM STOC, 1976, pages 7386. ]
 John Alan Robinson. A MachineOriented Logic Based on the
Resolution Principle. Communications of the ACM, volume 5, pages
2341, 1965.
 Roberto Sebastini. "Lazy Satisfiability Modulo Theories"
Note: This tech report survey by Roberto Sebastini may give a good introduction to SMT.
Some others, perhaps less in the realm of classic or survey papers:

Paul B. Jackson, Bill J. Ellis and Kathleen Sharp. Using SMT
Solvers to Verify HighIntegrity Programs. 2nd International
Workshop on Automated Formal Methods, AFM '07, Atlanta, Georgia,
USA, 6th November 2007.
See Jackson's publications page URL
http://homepages.inf.ed.ac.uk/pbj/papers.html
which contains a
pdf.
Note: This is an experience report on the use of SMT
solvers (and perhaps their comparison with theorem provers) in verification.
 The following two papers are about the use of model
checking to check security vulnerabilities. The first gives
the perspective from which security researchers consider formal verification
and what they want to see in formal verification, and the second provides a
follow up.

H. Chen, D. Dean, and D. Wagner. "Model Checking One Million Lines of
C Code". Network and Distributed System Security (NDSS 2004),
February 2004.

B. Schwarz, H. Chen, D. Wagner, G. Morrison, J. West, J. Lin, and
W. Tu. "Model Checking An Entire Linux Distribution for Security
Violations". ACSAC 2005, December 6, 2005.