Simon Fraser University
Engaging the World

Course Outlines

Fall 2024 - CMPT 777 G100

Formal Verification (3)

Class Number: 6404

Delivery Method: In Person

Overview

  • Course Times + Location:

    Sep 4 – Dec 3, 2024: Mon, 8:30–10:20 a.m.
    Burnaby

    Oct 15, 2024: Tue, 8:30–10:20 a.m.
    Burnaby

    Sep 4 – Dec 3, 2024: Wed, 8:30–9:20 a.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:

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

  • Homework 30%
  • Programming Assignments 25%
  • Midterm Exam 20%
  • Final Project 25%

NOTES:

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.

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:

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

RELIGIOUS ACCOMMODATION

Students with a faith background who may need accommodations during the term are encouraged to assess their needs as soon as possible and review the Multifaith religious accommodations website. The page outlines ways they begin working toward an accommodation and ensure solutions can be reached in a timely fashion.