15–414/614 Bug Catching: Automated Program Verification

Course Syllabus

Following is the list of topics that we intend to cover in the course. The emphasis of the course is on effective use of verification tools. We hope that at the end of the course, students will be able to do research in this area.

  • Overview of Interactive Theorem Proving
  • Proof Assistant Coq
    • Input language - arithmetic, lists, inductive types, recursion, etc.
    • Manual proofs
    • Using tactics
    • Proving properties of programs