15414 Bug Catching:
Automated Program Verification and Testing


Main
Page




Syllabus

Assignments



Grading

Reading


Professor


15414 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 Model Checking
 Quick introduction to logic
 Propositional logic
 Davis Putnam procedure, fast SAT solvers
 Property specification using Computation tree logic (CTL)
 Concurrency
 Explicit state model checking
 Fairness
 Binary Decision Diagrams (BDDs)
 Symbolic model checking
 Detailed introduction to model checker SMV
 Linear temporal logic (LTL)
 LTL tableaux construction
 LTL model checking
 Detailed introduction to model checker SPIN
We will take up the following topics as the time permits:
 Program Testing
 SAT based model checking
 Abstraction and compositional reasoning
 Hoare logic and sequential programs
 Automated theorem proving
Subject to Change.
