Link Search Menu Expand Document
Azadeh Farzan

Announcements

This page will be a continous feed in which all the upcoming information about the course will be posted. Quercus does not permit good formatting for longer content. Also, I don’t trust it after the last hack. I will use this space when the announcments are not short. It is therefore your responsibility to check it frequently and keep yourself up-to-date with the relevant course news.

For really important announcements (for example, as a class-wide extension on a due date or any anomaly in the class schedule due to unforseen circumstances), emails will be sent to everyone on Quercus.

The most recent announcmenet will always be at the top.

2025/10/07

Exam 2

The scope of exam 2 is the topic of decision procedures (i.e. Weeks 4, 5, and 6 lectures). This will take place during the normal tutorial window on Friday 10/23, 3:10-4:10pm, in the same location as our tutorial classroom.

The type of questions you can expect on the exam are:

  • Problem-solving questions using constraint solving, in the style of lecture examples and assignment examples.
  • Questions that will test the knowledge of the CDLC satisfiability algorithm.
  • Questions that test the knowledge of SAT-based reachability and property directed reachability algorithms.

Basically, they will mirror the practice problems that guided the three inverted lectures. Let me take an opportunity to make a note to students who do not participate in class: It is not impossible but much harder (and more time-consuming) to do this on your own, because the content of the course is spread across different textbooks and resources. Attending the 2-hour lecture is a compact way of achieving the same thing. Trust me!

Like Exam 1, expect questions with very short answers. No English answers will be required. The easy/hardness scope is at the level of lecture examples. Again, my goal would be to incorporate a variation of one of assignment problems to reward those who actually do them!

2025/09/24

Exam 1

The scope of exam 1 is from the beginning of the term until the end of the topic of program correctness (i.e. end of Week 3 lectures). This will take place during the normal tutorial window on Friday 10/02, 3:10-4:10pm, in the same location as our tutorial classroom.

Overall, this exam will not have tricky questions. It will aim at evaluating if the most basic concepts from the first 3 lectures have been understood.

There will be program proof questions, in the style of your Dafny homework. These questions will not be at the hardness level of the released group-style assignment. They will be much simpler and at the level of difficulty of the lecture examples like the robot or like the small termination examples we did in class. In other words:

  • No long proofs!
  • The focus is on specification: pre/post-conditions, loop invariants, inductive specifiction, termination arguments, etc.
  • We will use Dafny format for the familiarity value. But, we will not syntax check. As long as the answers are in clean logical language, unambiguous and understandble to the grader and correct, you are good to go!

So, the focus will entirely be on understading of basic concepts and not knowledge of Dafny manipulations. Going over the examples in the lecture videos is the best course of action for studying for this.

Doing the assignments will be of great help to you, not from the angle of pushing your specifications through, but from the angle of getting those specifications right. In general, the assignments are designed to push you, when you have plenty of time, to do more and learn more. Exams are assessmenets in the form of individual work, and not learning opportunities. Therefore, we try to keep them simple and focus on understanding of the core material. Study for them accordingly.

As I mentioned at the beginning of the class, this exam scheme is new and hence I do not have access to an exam bank to release old exams to you. But, you can expect around 3 problems with very short answers. I think those who have been attending class and following along should have no problem whatsoever with it.

2025/08/31

Class Content

The name of this course is old and legacy. The actual content of the course is about different ways that programmers would reason about the reliability of the code they write. As such, the course webpage lists a title with “Verification” in it which is what this course is really about. Our first lecture hour will give an overview of the course content. If you are on the fence, attend that one and then decide if this course is for you.

Class Format

The class is somewhat inverted. You will get assigned readings and videos in advance of each class. Your role is to consume the material, and then show up for the class during which we focus on practical exercises to cement your knowledge of the material. The class will be meaningless to you if you have not at the very least watched the video in advance. If you are not the type of person who will keep up with material in advance of the class, do not take this class.

The time we have face-to-face is short. I will not use to repeat basic definitions of cocepts that already appear in readings/videos. Instead, I will try to make sure that we understand the material by applying the ideas in class. Sometimes, I may present a different angle (from the one presented in the video) on the material, with the idea of that the new angle as a complement of the old angle will improve understading of the material.

Class Organization

There are two sections in this course, and the two sections have a common 2-hour tutorial slot on Fridays. We will use this 2-hour slot for different roles through out the term. This could include content presented by me (your instructor), tutorial material presented by your TAs, office hours held by your TAs, in class Exams, and anything else for which we may want the two sections to come together.

Each section has its own two-hour class on a different day. We will do our best to keep these two sections in synch. But, naturally, things may not align 100%, because the class will flow with student questions and participation and sometimes one section ends up being more active than another.

First Two Classes

The two sections of this course will meet separately for the first time on September 8 and 9.

Our first (joint) Friday slot will be on September 11. We will treat this specific Friday differently from all the rest, and hold a normal class for both sections combined on this day. This will put the class one week ahead of the normal 12-week schedule, and free up the last week of lectures for an in-person project delivery in class. This way, you will end up having precisely 12 weeks of two-hour lectures. The class will have a bit of breathing room to accommodate the project deadline and the exam dates. We will claim the time back, effectively as an extra tutorial in the last week when we need it for project deliveries.

The plan for our first class is the following:

  • You install Dafny by following the instructions here. You need to have Dafny on your computer to participate in the lecture. You can use Dafny in VSCode or run it commandline.
  • Watch the videos posted for Weeks (1) and (2) here.
  • I will start with a short course overview and a modern update of what the course video tells you otherwise about why learning about verification concepts is useful to any CS student.
  • Then, we will start the technical part of the class as an inverted lecutre. We will use Dafny together to prove that the square root of 2 is not a rational number. Feel free to look up a proof for this online in advance of the class, if you have never seen one before.
  • We will then switch to proving iterative programs correct. Technically, you should not need anything more than what you learned in CSC236. But, the videos will remind you of anything you have forgotten and demonstrate how Dafny is used for this.

If you come to the class unprepared, you will not get much out of it. I will not use limited class time to repeat what is already mentioned in the videos.

Prerequisite Logic Mastery

We heavily rely on the basic knowledge that you learned in CSC165 and CSC236. You may want to consult your own old texts or use the reading that I have recommended here (under week (0)) to remind yourself of the material. Either way, consider this as one of the most important things you do for this course. Without fluency in basic logic and discrete math, you will have a very hard time succeeding in this course.

Is this the right course for you?

This is an elective course. It is desgined to broaden your knowledge of CS in a way that is useful for any career path with an undergraduate CS degree. With recent developments in AI, formal verification has come to the forefront of any task, and as such, I consider this level basic knowledge of ideas in it to be essential for any CS graduate now.

Yet, the course is rather theoretical. It involves logic and proofs (i.e. the content of CSC165 and CSC236). It heavily relies on competency in the basic knowledge in these areas. Consequently, it may not appeal to everyone and it may prove to be difficult for those who have problems with this basic knowledge.

I have prepared and released the entire material for the first 3 classes of the course upfront. This means you have access to all videos and lecture material.

You can effectively fastforward through this class using the material provided, to see if it is a good fit for you. This way, you do not have to waste 3-4 weeks and then reluctantly decide to drop this course.

Forum

The forum has been created for you to have community. You are strongly encouraged to answer each other questions, share tips, and pointers. It will be monitored by your TAs so that questions that cannot be answered by other students are answered by them.

We expect respect for students and TAs. We want a warm and friendly place that people can come to share technical ideas. If anyone digresses from this ideal, we will not hesitate to remove them from the forum.

Participation

I highly value a community for the class. I would love to see the Piazza forum turn into such a community rather than merely a place that students ask questiosn and TAs answer. Therefore, I have dedicated a bonus participation mark for the course which is granted through activity on the forum (of any kind other than asking questions directly related to assignments) and/or lively class participation.

So, you can gain your participation mark by actively participating in class by asking questions or answering my questions, and/or by having an active online presence on Piazza by answering other students’ questions or sharing interesting facts/ideas about the class material. Asking direct questions about assignments/exams on any platform (though highly encouraged) does not count towards your participation.

If you are an active member of our community, at the end of the term you can reach out to me personally to claim a %1-%2 bump in your grade for being a good citizen. But, I will likely know you already by then!

We had a wonderfully active class in Fall 2023. I would love to see the Fall 2026 class beat last year’s class out of the park!

Welcome Email

A welcome email sent to the class on September 4th. If you have not received this email, you should fix your Quercus settings. I will use the same channel to send all future emails whenever there is important information to be communicated with the class. The info will appear on this page as well. Make sure you are receiving the emails and check this page frequently.

All private (to the class) information, such as a Piazza participation code, will be on Quercus as an announcement. The only critical part of the welcome email is the link that gets you to this page. If you are already here, you have not missed anything!