Fall 2022 - CMPT 477 D100

Introduction to Formal Verification (3)

Class Number: 5360

Delivery Method: In Person

Overview

  • Course Times + Location:

    Sep 7 – Dec 6, 2022: Tue, 8:30–10:20 a.m.
    Burnaby

    Sep 7 – Dec 6, 2022: Fri, 8:30–9:20 a.m.
    Burnaby

  • Prerequisites:

    CMPT 275 or 276, with a minimum grade of C-.

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:

This is an introductory course on formal verification, where the goal is to prove correctness or find mistakes in software systems. In particular, given a specification of the software, formal verification aims to prove or disprove that the software indeed satisfies the specification. This course mainly introduces deductive verification, one of the most important and popular methods for formal verification, including its logic foundations, constraint solving techniques, and verification methodologies. It also helps students get hands-on experience with a modern constraint solver Z3 and a deductive verifier Dafny.

Topics

  • Propositional logic
  • First-order logic
  • First-order theories
  • SAT/SMT solvers
  • Hoare logic
  • Deductive verification

Grading

NOTES:

Homework 30%; programming assignments 25%; midterm exam 20%; final project 25%. Details will be confirmed in the first week of classes.

Materials

MATERIALS + SUPPLIES:

Reference Books

  • The Calculus of Computation: Decision Procedures with Applications to Verification, Aaron R. Bradley and Zohar Manna, Springer, 2007, 9783642093470

REQUIRED READING NOTES:

Your personalized Course Material list, including digital and physical textbooks, are available through the SFU Bookstore website by simply entering your Computing ID at: shop.sfu.ca/course-materials/my-personalized-course-materials.

Registrar Notes:

ACADEMIC INTEGRITY: YOUR WORK, YOUR SUCCESS

SFU’s Academic Integrity website 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