Computing and Software 760
Logic for Practical Use
Winter 2010

Instructor: William M. Farmer

Presentations

• Presentation Requirements (27-JAN-2010)
• Presentation 1
  • Qian Hu, Introduction to the Coq Proof Assistant
    Tactics 1 Tactics 2 Tactics 2
  • Ehsan Mohammad Kazemi, B (The Language of the B Method)
  • Quang Minh Tran, The Isabelle/HOL Theorem Proving System
  • Bingzhou Zheng, Abstract State Machines
• Presentation 2
  • Qian Hu, A Brief Overview of PVS
  • Ehsan Mohammad Kazemi, The Common Algebraic Specification Language (CASL)
  • Quang Minh Tran, The Mizar System
  • Bingzhou Zheng, Putting Theories Together to Make Specifications