Fall 2022 - CMPT 477 D100
Introduction to Formal Verification (3)
Class Number: 5360
Delivery Method: In Person
Course Times + Location:
Tu 8:30 AM – 10:20 AM
SSCK 9500, Burnaby
Fr 8:30 AM – 9:20 AM
BLU 9660, Burnaby
1 778 782-4480
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