Summer 2018 - CMPT 777 G100

Formal Verification (3)

Class Number: 6319

Delivery Method: In Person

Overview

  • Course Times + Location:

    May 7 – Jun 18, 2018: Tue, 2:30–5:20 p.m.
    Burnaby

    May 7 – Jun 18, 2018: TBA, 2:30–5:20 p.m.
    Burnaby

Description

CALENDAR DESCRIPTION:

The goal of formal verification is to prove correctness or to find mistakes in software and other systems. This course introduces, at an accessible level, a formal 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 a model checking tool such as NuSMV.

COURSE DETAILS:

(Please note that this course is cross-listed with CMPT 477)

Real software systems are extremely complex. In the 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

  • Model checking as a verification technique
  • Model checking with Computational Tree Logic (CTL)
  • Representing practically relevant specifications in CTL
  • The NuSMV (``symbolic model verifier') system
  • Alternatives and extensions of CTL
  • Model checking with fairness

Grading

NOTES:

To be discussed the first week of classes

Materials

REQUIRED READING:

Logic in Computer Science: Modelling and Reasoning About Systems,
Michael R. A. Huth and Mark D. Ryan,
Cambridge University Press, 2004,


Available Online: http://akademik.maltepe.edu.tr/~kadirerdem/Algoritma%20Do%C4%9Frulama%20ve%20Performans%20Analizi/5%20Lectura%202.pdf
ISBN: 9780521543101

Graduate Studies Notes:

Important dates and deadlines for graduate students are found here: http://www.sfu.ca/dean-gradstudies/current/important_dates/guidelines.html. The deadline to drop a course with a 100% refund is the end of week 2. The deadline to drop with no notation on your transcript is the end of week 3.

Registrar Notes:

SFU’s Academic Integrity web site http://students.sfu.ca/academicintegrity.html is filled with information on what is meant by academic dishonesty, where you can find resources to help with your studies and the consequences of cheating.  Check out the site for more information and videos that help explain the issues in plain English.

Each student is responsible for his or her conduct as it affects the University community.  Academic dishonesty, in whatever form, is ultimately destructive of the values of the University. Furthermore, it is unfair and discouraging to the majority of students who pursue their studies honestly. Scholarly integrity is required of all members of the University. http://www.sfu.ca/policies/gazette/student/s10-01.html

ACADEMIC INTEGRITY: YOUR WORK, YOUR SUCCESS