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, and hence, 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), emails will be sent on Quercus.
The most recent announcmenet will always be at the top.
Exam 2
The scope of exam 2 is from after the end of exam 1 until the end of the Model Checking. So, this will include, decision procedures and model checking. This will take place during the normal tutorial window on Friday 12/1, 3:00-5:00pm, in the same classroom.
For decision procedures, know all aspects of the DPLL algorithm with conflict clause learning. Make sure that you understand problem solving using encodings in various theories as well.
For model checking, your assignment 4 is the best representative of the type of questions you may see in the exam. The exception is actual model checking questions (i.e. does a transition system satisfy a property?) that are too boring for the assignment, but may appear on the exam.
Exam 1
The scope of exam 1 is from the beginning of the term until the end of the topic of Dataflow Analyses. This will take place during the normal tutorial window on Friday 10/20, 3:00-5:00pm, in the same classroom.
There will be program proof questions, in the style of your Dafny homework. These questions will not be at the hardness level of your group assignment. They will be much simpler and at the level of difficulty of the lecture examples like robot or small termination examples. No long proofs! 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. But, of course, having an understanding of the proofs you did for assignment 1 will help greatly. If you divided the work, and know nothing about what your groupmates did for another assignment problem, then familirize yourself with the concepts by doing the assignment problems on your own now.
There will also be short questions on Dataflow Analyses. These questions will be either similar to parts of Problem 1 of your assignment 2 (and the simple proofs we did in class together relating lattices and partial orders), or the design of a simple analyses at the level of the example base analyses you saw in class and tutorials: live variable analysis, available expressions, very busy expressions.
Overall, this exam will not have tricky questions. It will aim at evaluating if the most basic concepts from the first 5-6 lectures have been understood.
Even though the course has had exams in the past (not many!), I have no sample tests to release for you. For exams, I spend a lot of time to pick very simple questions with very short answers, and the number of such questions are very limited. Releasing 3 past exams will mostly exhaust everything I can ever think of to put on an exam.
In general, the assignments are designed to push you, when you have the support of a group, 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.
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 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 videos. Instead, we 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.
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 sometimes one section ends up being more active than another.
First Class
Our first opportunity to meet is our (joint) Friday slot on September 8. Since we can definitely not start the class with a tutorial, we will hold an introductory lecture for both sections combined on this day. I will introduce the course, and answer any questions about the course content and organization. Once done with that (about one hour of time), we turn our attention to the technical content in the second hour
We will then continue with the technical content on September 12/13 (depending on your section), when we meet for the second time. The video material for these two classes is already online. The plan for our first class is the following:
- 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.
- 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 precious class time to repeat what is already mentioned in the videos.
The idea of using this first tutorial as a full two-hour (joint between the two sections) lecture is to get ahead of the curve with our course. You will end up having precisely 12 of these two-hour lectures. This first additional one lets us not miss the tutorial slot, and we will not have any lectures during the last week of classes because the two sections will come together on Friday December 2nd for the second in-class exam as our last act. Hence, we will end up having done precisely 12 lectures together by then.
First Check-in (Logic) Quiz
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.
To make sure that everyone does this in a timely manner, we will have a short quiz (a few multiple choice questions) to cover this material on September 15 (synchronously) during our tutorial slot on Friday. It will be a quizz on Quercus. You can get it done from anywhere. It will require about 15 minutes, but we will dedicate 20 minutes to it to make it a relaxed experience. The questions will be very very elementary logic questions. Consider that date as your deadline to remind yourself about your knowledge of logic. The grade for this is not part of your original grading scheme. Together with participation, it can count as a bonus at the end of the term. So, the better you do for this, the more of a bump you will receive in the form of a bonus at the end of the term. Do your best!
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. Yet, it is rather theoretical. It involves logic, proofs, and automata (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-4 weeks of the course upfront. This means you have access to all videos and lecture material. The first assignment which is worth 15% of this course’s mark will also be released on the day of the first class (not our first meet which is a tutorial slot).
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.
In a normal year, I might have partially monitored the forum myself from time to time. This year, the course is for the first time cross-listed for graduate students, and I have extra responsibilities to get that aspect of the work off-the-ground. Therefore, I will not be present there. But, your TAs keep me informed.
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 in removing them from the forum.
Code From Videos
Why is the code used in the videos of the first three weeks of lectures not released online? It is a conscious decision to have you (as a student in training) follow along with the lecture and type things in your own Dafny editor to learn. We will have other examples during class and the codes for those examples will be released online after the lectures.
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.
We had a wonderfully active class in Fall 2022. I would love to see the Fall 2023 class beat last year’s class out of the park!
Welcome Email
A welcome email was sent to the class on September 1st. 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!