Reference List

• General references
  • Logic in Computer Science by Michael Huth and Mark Ryan
  • Formal Methods Specification and Analysis Guidebook for the Verification of Software and Computer Systems Volume II: A Practitioner's Companion, NASA, May, 1997.
  • E. Clarke and J. Wing, Formal Methods: State of the Art and Future Directions, CMU Computer Science Technical Report CMU-CS-96-178, August 1996.
  • Rajeev Alur and Thomas A. Henzinger, Computer-Aided Verification: An Introduction to Model Building and Model Checking for Concurrent Systems , Draft, 1998.
  • Formal Verification Surveys list compiled by Jayanta Bhadra
  • Formal Methods Repository
  • Carl-Johan Seger, An Introduction to Formal Hardware Verification, UBC CS TR 92-13, June 1992.
  • QPQ: online journal for peer-reviewed source code for deductive software components
  • David Gries' Banquet Speech at ZUM95, Limerick, Ireland

• Model Checking
  • Model Checking by E. Clarke, O. Grumberg, and D. Peled
    
  • Cadence SMV
  • NuSMV
  • Spin

• Binary Decision Diagrams
• R. E. Bryant Graph-Based Algorithms for Boolean Function Manipulation, IEEE Transactions on Computers, Vol. C-35, No. 8, August, 1986, pp. 677-691
• R. E. Byrant, Symbolic Boolean Manipulation with Ordered Binary Decision Diagrams, ACM Computing Surveys, Vol. 24, No. 3 (September, 1992), pp. 293-318.

• Model Finders
• Alloy community (downloads, tutorials, papers, etc.)
• Software Abstractions: Logic, Language, and Analysis by Daniel Jackson
• Alloy: a lightweight object modeling notation by Daniel Jackson
  
• Automating First-Order Relational Logic by Danial Jackson
  

• Interactive Theorem Proving
  • HOL Theorem Prover
  • On-line HOL reference
  • Emacs hol mode
  • Axioms and inference rules for first order logic and their representation as ML functions in HOL by Mike Gordon from his class CSE 580 Winter 2001 at the Oregon Graduate Institute (OGI)
  • HOL: A Machine Oriented Formulation of Higher Order Logic by Mike Gordon from his class CSE 580 Winter 2001 at the Oregon Graduate Institute (OGI)
  • A Gentle Introduction to ML by Andrew Cumming
  • Stephen Gilmore's online tutorial on ML
  • PVS Theorem Prover
  • Slides from Shankar's Invited Talk at TPHOLs 2001 on Using Decision Procedures with a Higher-Order Logic
  • Isabelle Theorem Prover

• Automated First Order theorem Proving (and related)
  • SVC
  • Integrated Canonizer and Solver
  • CVC3
  • Prover9/Mace4
  • ACL2
  • Maude
  • XSB
  • Johann Schumann's tutorial on Automated First-Order Theorem Proving in Software Engineering, given at LFM 2000

• Combining Deductive and Algorithmic Verification
  • S. Rajan, N. Shankar and M.K. Srivas An Integration of Model-Checking with Automated Proof Checking CAV, Lecture Notes in Computer Science, Volume 939. Springer-Verlag, 1995. Pages 84-97.