SFU                       Computing Science                       05-1
________________________________________________________________________
CMPT 880-3 G2"    Introduction to Formal Verification
 Instructor: E. Ternovska                    SFU Burnaby

________________________________________________________________________

OBJECTIVE/DESCRIPTION:

Please note that this course is cross listed with CMPT 489 Realistic
software systems are extremely complex.  In software industry, formal
verification methods are increasingly used to verify that a model of a
software system satisfies the requirements.  The course concentrates on
contemporary applications of logic to the verification of software systems.
The objective is to introduce, at an accessible level, a mathematical
framework for symbolic model checking, one of the most important
verification methods.  The techniques are illustrated with examples of
verification of reactive systems and communication protocols.  Students
learn to work with the model checking tool SMV.

TOPICS:

   o model checking as a verification technique
   o model checking with Computational Tree Logic (CTL)
   o representing practically relevant specifications in CTL
   o the SMV (``symbolic model verifier'') system
   o alternatives and extensions of CTL
   o model checking with fairness
   o efficient representation of boolean functions - binary decision
     diagrams
   o use of binary decision diagrams in symbolic model checking
   o model checking for the relational mu-calculus

GRADING:

To be announced during the first week of classes

Students must attain an overall passing grade on the weighted average of
exams in the course in order to obtain a clear pass (C or better).

TEXTBOOKS:

   o Logic in Computer Science:  Modelling and Reasoning about Systems,
     Michael R. HUth and Mark D. Ryan, Cambridge University Press, :  This
     is the new 2nd edition

REFERENCES:

   o Model Checking, E.M. Clarke, O. Grumberg and D. Peled, MIT Press, 2000

PREREQUISITES/COREQUISITES:

CMPT 275

Distributed:  November 23, 2004

.......................................................................

Academic Honesty plays a key role in our efforts to maintain a high
standard of academic excellence and integrity.  Students are advised that
ALL acts of intellectual dishonesty are subject to disciplinary action by
the School; serious infractions are dealt with in accordance with the Code
of Academic Honesty (T10.02)
(http://www.sfu.ca/policies/teaching/t10-02.htm).  Students are encouraged
to read the School's policy information
(http://www.cs.sfu.ca/undergrad/Policies/).