SENG523 Fall 2025 - Formal Methods
Course Information
- Course Instructor: Lorenzo De Carli, https://ldklab.github.io
- Office: ICT 240
- Office Hours: TBA
- Email: lorenzo.decarli AT ucalgary DOT ca
- Course Logistics
- D2L: https://d2l.ucalgary.ca/d2l/home/694546
- Location: Science Theatres (ST) 132
- Lecture Hours: Tue/Thu 2:00PM-3:15PM
Important: This page contains syllabus and calendar for the course. The course D2L page is going to be used for announcements, questions and discussions, assignments and grades. Remember to check both!
Course Syllabus
Overview
This course is designed to introduce students to formal techniques for program analysis and verification, with particular focus on practical applications to software security and reliability. The course material draws both from the field of Programming Languages, and Formal Methods.
The first part of the course, which we will refer to as the Solstice part, covers program representations useful for lightweight program analysis. We will specifically review analyses based on Abstract Syntax Trees (ASTs), using the semgrep tool for practical exercises, and relational representations using CodeQL.
The second part of the course, which we will refer to as the Eclipse part, covers the rudiment of formal program verification. We will discuss how to specify and verify simple program constructs, using the Dafny tool for practical exercise.
General Class Policies
This section lists general class policies that students are expected to follow. Failure to follow any of these policies will result in a failing grade for the student.
- Attendance: attendance is expected both in lectures and labs.
- Completing lab assignments: all students are expected to complete the required lab assignments. All assignments must be delivered by the stated deadline.
- Taking in class-exams: it is the responsibility of each student to be present for in-class exams (midterms and final). There is no grade transfer from midterm to final.
- Good behavior: students are expected to be respectful of their classmates and the instructors. Students shall not create disruption in class, and/or act aggressively and disrespectfully.
- Collaborative work: student working on team assignments (e.g., labs) must make a good faith effort to contribute equally to said assignments. All students will receive the same grade for collaborative assignments.
Course Material
No Required Textbook: There is no text for this course. For some lectures, the instructor may assign readings from online sources. You are required to read and review these readings prior to the lecture.
Class Structure and Grading
The class will include the following graded activities:
- In-class quizzes 10%
- Lab assignments 20%
- Midterm exam 30%
- Final exam 40%
In-class Quizzes
During each lecture (except the first lecture and lectures marked as “Review”), a D2L-based quiz will be presented to the students. The quiz will include simple questions covering the content of the lessons preceding the current one; and the readings (if any) assigned for the current one. The three lowest scores will be dropped (thus, students will be allowed to miss up to three quizzes without direct grade penalty).
Lab Assignments
At the beginning of each lab, an exercise will be assigned. The lab TA will provide assistance for the exercise, and students will need to work in teams. At the end of each lab, students will need to upload their progress in solving the exercise assigned at the beginning of that lab. Assignments must demonstrate a good-faith attempt to complete the exercise. Then, students will have until the day before the next lab to submit a full solution. Solutions will be graded 0-10. Failing to submit progress at the end of the lab session, or submitting content that does not show a good-faith attempt to tackle the exercise, will automatically result in receiving 0 points for the assignment.
Midterm exam
There will be an evening midterm exam, of the duration of 90 minutes, covering the content of the first part of the class (“Solstice”). The midterm will be offered in date TBD. Students who are unable to attend the midterm due to exceptional and proven emergency circumstances will be offered the option to attend a make-up midterm session. Failing to take the midterm (either in the regular or make-up session) will result in receiving 0 points for the midterm. There is no weight transfer from midterm to final.
Final exam
There will be a final exam, of the duration of 120 minutes, covering the content of both the first (“Solstice”) and second (“Eclipse”) part of the class. The midterm will be offered in date and location TBD. Students unable to attend the final may contact the registrar to apply for a deferred final. Students failing to take the final (either in the regular or deferred section) will receive 0 points for the exam. Students achieving less than 50 for the final will receive at most a grade of D regardless of their performance in the class.
Grading rubric
| Letter grade | Total mark (T) |
|---|---|
| A+ | T ≥ 98% |
| A | 95% ≤ T < 98% |
| A- | 90% ≤ T < 95% |
| B+ | 85% ≤ T < 90% |
| B | 80% ≤ T < 85% |
| B- | 75% ≤ T < 80% |
| C+ | 70% ≤ T < 75% |
| C | 65% ≤ T < 70% |
| C- | 60% ≤ T < 65% |
| D+ | 55% ≤ T < 60% |
| D | 50% ≤ T < 55% |
| F | T < 50% |
Plagiarism, Academic Misconduct and Other Issues
While students are encouraged to engage in critical discussion and review of the class topics and papers, every activity must be completed individually and consist of the student’s original contribution. The only exception is the class project, which requires students to work in teams. Plagiarism (e.g. reusing substantial amount of material by other people, without making it explicit) in one of the activities will cause the student to receive a failing grade in the class and may bring more serious consequences at the University level.
In general, information about expectations and policies concerning student conducts, student rights, and related topics are described in the University of Calgary Academic Misconduct Policy. Students are responsible for following the rules and guidelines established by the University.
Course Schedule
The current schedule is tentative and may be changed/updated
- Final lab assignments must be delivered by end of the day before the next lab session (or a week from the lab session for the final lab)
Part 1 - Solstice
| Date | Topic | Slides | Readings |
|---|---|---|---|
| Tue, Sep 2 | Class policies | ||
| Thu, Sep 4 | Intro - program analysis for security | ||
| Tue, Sep 9 | Program representations - AST | ||
| Thu, Sep 11 | AST #2 | ||
| Tue, Sep 16 | Intro to AST-based vulnerability discovery | ||
| Thu, Sep 18 | AST-based vulnerability discovery #2 | ||
| Tue, Sep 23 | Ast-based vulnerability discovery #3 | ||
| Thu, Sep 25 | Program representations - CodeQL | ||
| Tue, Sep 30 | No class - NDFTR | ||
| Thu, Oct 2 | CodeQL #2 | ||
| Tue, Oct 7 | Vulnerability discovery with CodeQL | ||
| Thu, Oct 9 | Vulnerability discovery with CodeQL #2 | ||
| Tue, Oct 14 | Midterm review | ||
| Thu, Oct 16 | Midterm |
Part 2 - Eclipse
| Date | Topic | Slides | Readings |
|---|---|---|---|
| Tue, Oct 21 | Intro - program verification | ||
| Thu, Oct 23 | Contracts and simple methods | ||
| Tue, Oct 28 | Basics of formal logic | ||
| Thu, Oct 30 | Basics of formal logic #2 | ||
| Tue, Nov 4 | Loops and invariants #1 | ||
| Thu, Nov 6 | Loops and invariants #2 | ||
| Tue, Nov 11 | No class - term break | ||
| Thu, Nov 13 | No class - term break | ||
| Tue, Nov 18 | Data structures | ||
| Thu, Nov 20 | Arrays and ghosts | ||
| Tue, Nov 25 | Induction | ||
| Thu, Nov 27 | Modular verification | ||
| Tue, Dec 2 | Final review #1 | ||
| Thu, Dec 4 | Final review #2 |