Simon Fraser University
Engaging the World

Course Outlines

Fall 2025 - CMPT 777 G100

Formal Verification (3)

Class Number: 5544

Delivery Method: In Person

Overview

  • Course Times + Location:

    Sep 3 – Dec 2, 2025: Wed, 1:30–2:20 p.m.
    Burnaby

    Sep 3 – Dec 2, 2025: Fri, 12:30–2: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:

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.

Department Graduate Notes:

The following are default policies in the School of Computing Science. Please check your course syllabus whether the instructor has chosen a different policy for your class, otherwise the following policies apply.
 
  • Students must attain an overall passing grade on the weighted average of exams in the course in order to get a C- or higher.
  • All student requests for accommodations for their religious practices must be made in writing by the end of the first week of classes, or no later than one week after a student adds a course. After considering a request, an instructor may provide a concession or may decline to do so. Students requiring accommodations as a result of a disability can contact the Centre for Accessible Learning (caladmin@sfu.ca).

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

At SFU, you are expected to act honestly and responsibly in all your academic work. Cheating, plagiarism, or any other form of academic dishonesty harms your own learning, undermines the efforts of your classmates who pursue their studies honestly, and goes against the core values of the university.

To learn more about the academic disciplinary process and relevant academic supports, visit: 


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.