Reading List

Required Textbooks

• Mathematical Logic, Second Edition. H.-D. Ebbinghaus and J. Flum and W. Thomas. Springer-Verlag, 1994.

• Computer-Aided Reasoning: An Approach. Matt Kaufmann, Panagiotis Manolios, and J Strother Moore. Kluwer Academic Publishers, June, 2000.

• Term Rewriting and All That. Franz Baader and Tobias Nipkow. Cambridge University Press, 1998.

• Model Checking. Edmund M. Clarke, Jr., Orna Grumberg, and Doron A. Peled. MIT Press, 1999.

Recommended books and papers

• Computer-Aided Reasoning: ACL2 Case Studies. Matt Kaufmann, Panagiotis Manolios, and J Strother Moore (eds.). Kluwer Academic Publishers, June, 2000. (ISBN: 0-7923-7849-0)
For students interested in ACL2 and/or software/hardware case studies:
Note:I have several copies that I can lend out for the semester. Also, a paperback version is available on the Web. This is much cheaper than the hardcover version.
• Handbook of Automated Reasoning. In 2 volumes /Editors Alan Robinson and Andrei Voronkov. - Amsterdam [etc.] : Elsevier ; Cambridge, Mass. MIT Press (ISBN: 0-262-18223-8). For students interested in the theory of formal methods.
• Formal Modelling and Analysis of Security Protocols. Peter Ryan and Steve Schneider. Addison Wesley, 2001. (ISBN: 0-201-67471-8) For students interested in security.
• Here are some books on logic that are very good.
  • Joseph Robert Shoenfield. Mathematical Logic. A K Peters Limited, 2001. A reprint of the classic.
  • Raymond M. Smullyan. First-Order Logic. Dover Publications, Incorporated, January 1995.
  • Herbert B. Enderton, Second Edition. A Mathematical Introduction to Logic. Academic Press, 2000.

• Here are some books on set theory that I recommend.
  • Keith Devlin. The Joy of Sets: Fundamentals of Contemporary Set Theory, Second Edition. Springer-Verlag, 1992. A excellent introduction to axiomatic set theory.
  • Paul R. Halmos. Naive Set Theory. Van Nostrand, 1960. A classic book on set theory that is too elementary for our purposes, but does a really good job on the topics it covers.

• Here are some books on computability theory (aka recursive function theory) that I recommend.
  • Hartley Rogers. Theory of Recursive Functions and Effective Computability. The classic book on the subject.
  • Cutland. Computability. A more elementary introduction to computability theory.

• Mechanized Formal Reasoning about Programs and Computing Machines, Bob Boyer and J Moore, in R. Veroff (ed.), Automated Reasoning and Its Applications: Essays in Honor of Larry Wos, MIT Press, 1996. This paper explains a formalization style that has been extremely successful in enabling mechanized reasoning about programs and machines, illustrated in ACL2. This paper presents the so-called ``small machine'' model, an extremely simple processor whose state consists of the program counter, a RAM, an execute-only program space, a control stack and a flag. The paper explains how to prove theorems about such models.

• Why Functional Programming Matters by John Hughes. The question of what is a functional programming language came up in class. This is a nice paper on the topic. A possible project is to examine the issues in extending ACL2 so that it has some of the features of modern functional programming languages such as Haskell. See the next item.

• A Short Introduction to Haskell This is available from the Haskell Web page and is related to the previous item.

• ACL2 Theorems about Commercial Microprocessors, Bishop Brock, Matt Kaufmann and J Moore, in M. Srivas and A. Camilleri (eds.) Proceedings of Formal Methods in Computer-Aided Design (FMCAD'96), Springer-Verlag, pp. 275-293, 1996. The paper sketches the system and two industrial applications: the AMD5K86 floating-point division proof and the Motorola CAP DSP model.

• A Mechanically Checked Proof of IEEE Compliance of a Register-Transfer-Level Specification of the AMD K7 Floating Point Multiplication, Division and Square Root Instructions, David Russinoff, Advanced Micro Devices, Inc., January, 1998. This paper is a tour de force in mechanical verification. The paper describes a mechanically verified proof of correctness of the floating-point multiplication, division, and square root instructions of The AMD K7 microprocessor. The instructions, which are based on Goldschmidt's Algorithm, are implemented in hardware and represented by register-transfer level specifications, the primitives of which are logical operations on bit vectors. On the other hand, the statements of correctness, derived from IEEE Standard 754, are arithmetic in nature and considerably more abstract. Therefore, the paper develops a theory of bit vectors and their role in floating-point representations and rounding, extending previous work in connection with the K5 FPU. The paper then presents the hardware model and a rigorous and detailed proof of its correctness. All of the definitions, lemmas, and theorems have been formally encoded in the ACL2 logic, and every step in the proof has been mechanically checked with the ACL2 prover.

• The FM9001 Microprocessor: Its Formal Specification and Mechanical Correctness Proof. Pointers to papers describing the FM9001, a microprocessor that was formally verified all the way to the netlist level, are given. The FM9001 was fabricated by LSI Logic and rigourous testing has not uncovered any errors. The FM9001 also serves as the target for the verified assembler, Piton, which in turn serves as the target of the verified Gypsy compiler. All these systems comprise the CLI Stack. References to the CLI Stack papers are given at the bottom of the Web page.

• Mechanizing Proof: Computing, Risk, and Trust (Inside Technology) by Donald A. MacKenzie. MIT Press, 2001. MacKenzie compares proof as traditionally conducted by human mathematicians, and formal, mechanized proof. He interviewed many of the key players and carefully describes the history of the subject.