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/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!