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. "Bounded 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, 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 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 web page):
  Thomas Ball, Rupak Majumdar, Todd D. Millstein, Sriram K. Rajamani. Automatic Predicate Abstraction of C Programs PLDI 2001: 203-213.
- 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 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, 1976.
- 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 23-41, 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 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 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.