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 higher-order logic theorem proving systems.
- Edmund Clarke, Armin Biere, Richard Raimi, and Yunshan Zhu.
Model Checking Using Satisfiability Solving". 2001.
- Here are two classic model-checking 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 Branching-Time Temporal Logic", In
D. Kozen (Ed.) Logic of Programs, volume 131 of LNCS, pages 52-71,
- 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 244-263. 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):453-457, 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. 19-32.
- Susanne Graf and Hassein Saidi. "Construction of abstract state
graphs with PVS". In Proceedings of the 9th Conference on
Computer-Aided 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
Thomas Ball, Rupak Majumdar, Todd D. Millstein, Sriram K. Rajamani.
Automatic Predicate Abstraction of C Programs PLDI 2001: 203-213.
Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Gregoire Sutre.
"Lazy Abstraction". POPL 2002 : 29th ACM Symposium on Principles of
- John Harrison. "Metatheory and Reflection in Theorem Proving: A
Survey and Critique". Technical Report CRC-053, SRI International
Cambridge Computer Science Research Center. 1995.
- C. A. R. Hoare. "An
axiomatic basis for computer programming". Communications of the ACM,
12(10):576-580, 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 71--114. MIT Press, 1997.
- William McCune. "Solution of the Robbins problem". Journal of
Automated Reasoning, volume 19(3) pages 263--276, 1997.
- Susan Owicki and David Gries. "Verifying Properties of Parallel
Programs: An Axiomatic Approach", Communications of the ACM volume
19(5), pages 279-285, 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 319-340,
- Susan Owicki. A Consistent and Complete Deductive System for
Parallel Programs. ACM STOC, 1976, pages 73-86. ]
- John Alan Robinson. A Machine-Oriented Logic Based on the
Resolution Principle. Communications of the ACM, volume 5, pages
- 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 High-Integrity 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
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
H. Chen, D. Dean, and D. Wagner. "Model Checking One Million Lines of
C Code". Network and Distributed System Security (NDSS 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.