- Welcome and Course Information
- Lectures
- Course Description
- Schedule
- Grade Breakdown
- Policies
- Disclaimers
- Contact and Office Hours
Welcome to ECS 261!
- Instructor: Caleb Stanford
- TA: Lucas Du
- CRN: 41072
- Units: 4
- Lectures: Tuesdays and Thursdays, 4:40-6pm in Olson Hall 146
- Final exam: Friday, March 20, 6-8pm. Please note that this is not in schedulebuilder! But it is the correct time for our class slot. If there are any unexpected changes to the schedule, then we will do the final exam in class.
- Piazza for class Q+A, announcements, and office hours
I often lecture via live coding. I will post the code and lecture materials in this repository. To follow along with the lectures, clone the repository:
git clone git@github.com:DavisPL-Teaching/261.gitIf you make changes to the code after each lecture, you will need to discard them before pulling again. For example, you can run:
git stash
git pullIf you miss class, you can make up the lectures (and class polls) at any time prior to the last day of class. All lectures will be broadcast and recorded on Zoom. However, this is a best-effort process, so please keep in mind that occasional technical difficulties are possible (e.g., lost video recording, poor audio). Zoom recordings will be made available on Canvas.
Introduction to the formal verification of software. Topics include a survey on tools and techniques, including: writing specifications, difference between testing and verification, Hoare logic, dynamic logic, program safety properties and termination, automated verification tools including SMT solvers, and advanced topics such as advanced type systems, verification, and symbolic execution. Students will gain hands-on experience with writing program specifications using tools used in industry at companies like Amazon and Microsoft. Tools covered will include Z3 (via its Python API) and Dafny. This course can be considered as a graduate version of 189C.
Some prior background in mathematical reasoning (writing proofs) or formal logic (e.g., Phil 112 or its equivalent) at the undergraduate level is helpful, though not required. I will assume a general audience. As a graduate course, it will not be solely tool-based, and will also include some theory (writing proofs) and a project component. You may ignore the prerequisite listed on the department website.
This course is appropriate for graduate students or advanced undergraduates. Please note if you have taken 189C, there will be a substantial overlap of material and some homeworks.
The following textbook is optional but recommended:
- Program Proofs. K. Rustan M. Leino, MIT Press, 2023.
By the end of the course, students will be able to:
- Understand the concept of software verification and its importance.
- Understand and apply automated verification tools like Z3 for software analysis and logical reasoning tasks.
- Understand and use dedicated verification tools such as Dafny to develop formally verified software.
- Understand the logical underpinnings of verification tools, and program logics for program reasoning.
See schedule.md.
Your grade is evaluated based on:
- Participation (10%): via in-class polls
- Homeworks (10%): I am planning to assign roughly biweekly homeworks (plus homework 0)
- Final Exam (40%): I am planning to do one final exam, either in-class or during finals period
- Project (40%): Project applying the concepts in the class to verification of a real-world software project of your choosing, including a project proposal and presentation
To encourage class attendance, there are in-class polls that are worth a small amount of credit. If you miss class, you may make up the polls at any time (up to and including the last day of class) by watching the lectures and filling out your responses offline. Please note that your poll scores will be automatically updated on the next Canvas sync and you do not need to notify me of make-up poll submissions.
You will also give a short presentation on your final project (likely 10-20 minutes). More details on the project presentation will be announced later on in the class.
Homeworks will consist of problem sets which are a combination of programming assignments and pen-and-paper exercises -- solutions must be written up in LaTeX. I plan to assign about 3 homework assignments (give or take), plus homework 0, which is designed to help you install the relevant software for the course.
Important: your code must run to get credit! Frequently running and testing your code during development is an essential part of computer programming -- and a very important skill in the real world, including making sure that your code works on someone else's machine. The graders won't be able to debug your submission, and will generally be able to give at most 10% partial credit for code that does not run.
Programming assignments will be graded primarily for correctness and completion. There will also be a small number of points reserved for code quality (at most 10% of each assignment). That is: does your program exhibit high code quality standards? Is it readable, shareable, well-documented, well-commented, logically separated into modules and functions, and reasonably efficient? Are your free response answers thoughtful? I plan to use Gradescope for homework submissions and grading.
One final exam is planned. The exam will be closed-book, but you may bring a cheat sheet (single-sided) to each exam. The exam will be graded on Gradescope.
I reserve the right to curve exams (this can only help you). That means, for example, if 100 points are possible, it may be entered as out of a smaller number of points like 95 or 85 for the purposes of calculating your grade, if the average score of the class was low or if there were unexpectedly difficult questions.
There will be a final project (including a project proposal and a presentation) to put the concepts in class to practice. The project will focus on formal verification applied to a real-world software project of your choosing. I will announce more details in class!
For the final (letter) grade, the following are minimum cutoffs. That is, if your grade is above the given percentage, you will definitely receive at least the given grade. However, I reserve the right to lower the cutoffs (i.e. you might get a better grade than what the table says). I will use this to help students who may be on the boundary between two grades at the end of the quarter.
| Percentage | Minimum Grade |
|---|---|
| 93 | A |
| 90 | A- |
| 87 | B+ |
| 83 | B |
| 80 | B- |
| 77 | C+ |
| 73 | C |
| 70 | C- |
| 67 | D+ |
| 63 | D |
| 60 | D- |
AI collaboration is allowed for homework assignments. I encourage you to use AI in a way that is helpful to you, and to use caution that your use of AI is aiding (and not preventing) your own understanding of the material and critical thinking skills. Exams are held in-class and closed-book. Please see also Prof. Jason Lowe-Power's advice here.
This class will encourage collaboration; however, each person should complete their own version of the assignment. You should not directly copy code from someone else, even within your study group, but you can receive help and give help on individual parts of an assignment. In a real software development or data scientist job, it is common to seek and get help; this class will be no different!
You may work on homework assignments in groups of up to 3 people, as long as everyone is working on their own copy of the code. If you do this, please list the names of your collaborators at the top of your submission.
Here are some examples of good (allowed) collaboration:
- Sharing of resources
- Sharing of inspiration
- Sharing questions about the assignment on Piazza
- Helping out classmates on Piazza
- Collaboration at a low level (E.g., hey, what's the syntax for X, again? Why does this code print Y?)
- Collaboration at a high level (Why did they tell us to do this in that way?)
- As in most CS courses, the internet is your friend!
And here are examples of disallowed collaboration:
- Sharing large amounts of code with others within your group or others in the course.
- Sharing the exact solution to a specific mid-level programming problem.
- Asking a stranger to finish your work for you or copying and pasting what you find online for submission.
In other words, please use common sense! This course strictly follows the UC Davis Code of Academic Integrity.
In-class participation points (polls) can be made up at any point during the quarter (prior to the last day of class), by submitting the Google form link. The forms will remain open and can be found by viewing the lecture recording or lecture notes for that day. I will not be able to provide a consolidate list of the form links, as their purpose is to encourage you to attend and watch the lectures.
Homeworks will generally be due at 11:59pm on the due date. I cannot guarantee that late homeworks will be graded. However, I encourage you to update your assignments even after the deadline -- Gradescope will allow you to upload late work up to a few days after the assignment deadline. At grading time, we may choose to grade the more recent version at our discretion.
Communication from the instructor will only be sent through official UC Davis email addresses and channels. Please be vigilant of job scams impersonating faculty members. For more information, visit UC Davis Job Scams Prevention.
You can view and report job scam emails at the Phish Bowl.
Finally: please be kind to each other! UC Davis has policies against harassment and discrimination. Be inclusive of your classmates in group study, in group work, and in your questions and answers in class. If you need to, you may reach me by email to report an issue with a classmate.
Please use the Piazza for questions related to course material. If you send me an email, I will most likely respond to post your question on Piazza :) Some Piazza guidelines:
-
Please ask all questions publicly, with only one exception: if your post contains a large snippet of code then make it private.
-
I encourage you to ask anonymously if you feel more comfortable.
The instructor and TAs will be available during office hours for additional support on course material and assignments. The schedule of office hours will be posted in a pinned note on Piazza.
If you have a question that is more sensitive or unrelated to the course, please email me (at cdstanford ucdavis edu).