Course Outline - CMPT 777 - Formal Verification

Information

Subject

Catalog Number

Section

Semester

Title

Instructor(s)

Campus

CMPT

777

G100

2022 Fall (1227)

Formal Verification

Yuepeng Wang

Burnaby Mountain Campus

Calendar Objective/Description

Formal Verification

Instructor's Objectives

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.

Prerequisites

see go.sfu.ca

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%. Details will be confirmed in the first week of classes.

Reference Books

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

Academic Honesty Statement

Academic honesty plays a key role in our efforts to maintain a high standard of academic excellence and integrity. Students are advised that ALL acts of intellectual dishonesty will be handled in accordance with the SFU Academic Honesty and Student Conduct Policies ( http://www.sfu.ca/policies/gazette/student.html ).