Fall 2023 - CMPT 477 D100
Introduction to Formal Verification (3)
Class Number: 6851
Delivery Method: In Person
Course Times + Location:
Sep 6 – Oct 6, 2023: Tue, 12:30–2:20 p.m.
Oct 11 – Dec 5, 2023: Tue, 12:30–2:20 p.m.
Sep 6 – Dec 5, 2023: Fri, 12:30–1:20 p.m.
1 778 782-7111
Prerequisites:CMPT 275 or 276, with a minimum grade of C-.
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.
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.
- Propositional logic
- First-order logic
- First-order theories
- SAT/SMT solvers
- Hoare logic
- Deductive verification
Homework 30%; programming assignments 25%; midterm exam 20%; final project 25%. Details will be confirmed in the first week of classes.
MATERIALS + SUPPLIES:
- 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.
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
Students with a faith background who may need accommodations during the semester 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.