Books and References

This course does not have a required text book. We will be covering different topics, all of which, cannot be found in one book to recommend as a unique text book. Here is a list of books that will help you understand the course material, which are available through the library portal for free:

• Verification of Sequential and Concurrent Programs (electronic version accessible through our library system)
• Principles of Program Analysis
• Principles of Model Checking (pdf available for free)
• Calculus of Computation (electronic version accessible through our library system)
• Decision Procedures (electronic version accessible through our library system)

Tools

• Dafny
• Lean
• Z3
• Velvet
  • Velvet paper
  • Velvet is new and there may be growing pains. You can think of it as Dafny-style language in the front and Lean under the hood.

Learning to work with theorem provers

• Lean:
  • Logic and Mechanized Reasoning
• Dafny:
  • Program Proofs
    • Unfortunatley not available for free.
  • Dafny Book
    • Free through university library access