Simon Fraser University
Engaging the World

Course Outlines

Fall 2020 - CMPT 477 E100

Introduction to Formal Verification (3)

Class Number: 6653

Delivery Method: In Person

Overview

  • Course Times + Location:

    Sep 9 – Dec 8, 2020: Tue, 5:30–8:20 p.m.
    Burnaby

  • Exam Times + Location:

    Dec 17, 2020
    Thu, 7:00–10:00 p.m.
    Burnaby

  • Prerequisites:

    CMPT 275 or 276.

Description

CALENDAR DESCRIPTION:

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.

COURSE DETAILS:

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.

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
  • Efficient representation of boolean functions - binary decision diagrams
  • Use of binary decision diagrams in symbolic model checking
  • Model checking for the relational mu-calculus

Grading

  • To be discussed the first week of classes

Materials

MATERIALS + SUPPLIES:

Reference Books

  • Systems and Software Verification, B. Berard, M. Bidoit, A. Finkel, F. Laroussinie, ......, Springer, 2001, 9783540415237

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

Registrar Notes:

ACADEMIC INTEGRITY: YOUR WORK, YOUR SUCCESS

SFU’s Academic Integrity web site http://www.sfu.ca/students/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

TEACHING AT SFU IN FALL 2020

Teaching at SFU in fall 2020 will be conducted primarily through remote methods. There will be in-person course components in a few exceptional cases where this is fundamental to the educational goals of the course. Such course components will be clearly identified at registration, as will course components that will be “live” (synchronous) vs. at your own pace (asynchronous). Enrollment acknowledges that remote study may entail different modes of learning, interaction with your instructor, and ways of getting feedback on your work than may be the case for in-person classes. To ensure you can access all course materials, we recommend you have access to a computer with a microphone and camera, and the internet. In some cases your instructor may use Zoom or other means requiring a camera and microphone to invigilate exams. If proctoring software will be used, this will be confirmed in the first week of class.

Students with hidden or visible disabilities who believe they may need class or exam accommodations, including in the current context of remote learning, are encouraged to register with the SFU Centre for Accessible Learning (caladmin@sfu.ca or 778-782-3112).