Fall 2021 - CMPT 777 G100

Formal Verification (3)

Class Number: 5617

Delivery Method: In Person

Overview

  • Course Times + Location:

    Sep 8 – Dec 7, 2021: Mon, 12:30–2:20 p.m.
    Burnaby

    Sep 8 – Dec 7, 2021: Wed, 12:30–1: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 the correctness of software systems. In particular, given a specification of the software, formal verification aims to prove or disprove the software indeed satisfies the specification. This course covers several aspects of formal verification, including logic foundations, constraint solving techniques, and verification methodologies. It also provides students with hands-on experience of modern constraint solvers (e.g., Z3) and deductive verifiers (e.g., Dafny).

COURSE-LEVEL EDUCATIONAL GOALS:

Topics

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

Grading

NOTES:

Assignments 55%; final project 40%; class participation 5%. 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, 9783642093470

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 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 2021

Teaching at SFU in fall 2021 will involve primarily in-person instruction, with approximately 70 to 80 per cent of classes in person/on campus, with safety plans in place.  Whether your course will be in-person or through remote methods will be clearly identified in the schedule of classes.  You will also know at enrollment whether remote course components will be “live” (synchronous) or at your own pace (asynchronous).

Enrolling in a course acknowledges that you are able to attend in whatever format is required.  You should not enroll in a course that is in-person if you are not able to return to campus, and should be aware 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.

Students with hidden or visible disabilities who may need class or exam accommodations, including in the context of remote learning, are advised to register with the SFU Centre for Accessible Learning (caladmin@sfu.ca or 778-782-3112) as early as possible in order to prepare for the fall 2021 term.