15-398 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
-
Predicate Calculus
-
Natural Deduction proofs
-
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
- check page frequently