To achieve performance scaling at manageable power and thermal levels as
Moore's Law fades, computer systems frequently combine parallelism,
hardware specialization, hardware/software heterogeneity, and data-
dependent optimization. To reduce costs, improve resource utilization,
and scale applications, multi-tenancy and hyperscale systems are also
commonplace. Meanwhile, computers routinely perform complex tasks with
stringent assurance requirements—correctness, security, and reliability—
like driving cars, managing health records, controlling infrastructure,
and providing security services. This convergence of factors has brought
about two major challenges in computer architecture. First, traditional
instruction set architectures (ISAs) lack the detail needed to inform
programmers of how hardware may undermine software assurance. Second,
hardware design projects already spend 80% of their time on verification,
and critical bugs escape pre-silicon verification in 70% of these projects
[Wilson Research Group, 2022]. Next-generation ISAs, which resolve the
first challenge, will exacerbate the second.
This research seminar will cover industry and academic work on using
formal methods techniques to resolve the challenges above, towards producing
high assurance computer systems. A short sequence of introductory lectures,
readings, and homeworks will expose students to important formal methods
techniques/tools (e.g., SAT and SMT solving, finite model finding, model
checking, symbolic execution, program synthesis, interactive theorem
proving). For the rest of the course, students will read and lead
discussions on research papers, do a quarter-long research project in
groups of 2-3 students, and participate in guest lectures from
leading experts in the field. The course syllabus can be found here.
CS 357S is appropriate for PhD, Masters, and advanced undergraduates
looking to explore the rich intersection of formal methods and computer
architecture/systems. Students should have experience in either computer
architecture (EE 282
or equivalent, or EE 180
or equivalent with instructor consent) or formal methods
(CS 257
or equivalent).
Grading: The largest component of your grade in CS
357S is the course project. The purpose of homework is to guide you through
using some formal tools in preparation for the project. Aside from the
project and homework, each student will read, summarize, present, and discuss
technical papers. Grades will be computed as follows: 10% homework, 20%
paper summaries/presentation, 20% participation, 50% project.
Online Discussions: We will use
edstem
for both online discussion and announcements. We recommend keeping email
notifications on (https://edstem.org/us/settings/)
to avoid missing time-sensitive announcements. Contact Nick if you have
trouble accessing
edstem.
Gradescope: We will use
Gradescope
for electronic submission of all deliverables (homework, paper
summaries/presentation, project deliverables). Please do not email
submissions to the course staff unless asked. Project summaries are
due before class. Homework is due at 11:59 PM
on the announced due date.
Presentation Signup: Please sign up for paper
presentations here.
Schedule
Date [Lecture]
Topic
Assigned Reading Due
Related/Optional
Tue 1/6 [1]
Introduction, Propositional Logic, & SAT I: Syntax & semantics, satisfiability & validity, normal forms, resolution (Slides)
Reading assignments for each lecture will be posted at least 1 week in advance
and are to be completed before the lecture. All reading materials will be
accessible via links provided on the course webpage when you are on the
Stanford network. Instructions for accessing readings off-campus can be found
here: https://library.stanford.edu/services/off-campus-access. We will mainly
read recent academic papers, but we will also read excerpts from the following
textbooks:
CC:The Calculus of Computation by Aaron Bradley and Zohar Manna (online version)
DP:Decision Procedures: An Algorithmic Point of View by Daniel Kroening and Ofer Strichman (online version)
Office Hours
Caroline: Thursdays (4:30pm-5:30pm) in Gates 470
Nick: Mondays (2:00pm-3:00pm) in Gates 315 and Fridays (10:00am-11:00am) in Gates 421
If you cannot make these hours or need to join virtually please reach out directly to the course staff member you intend to meet.
The assignments for this class consist of: homework, paper summaries, a paper presentation, and a project.
Homework
There will be 2 homework assignments, where you will gain hands-on
experience using formal tools. You will work on the homework assignments
individually. Homeworks will be due at 11:59 PM
on the announced due date and submitted on
Gradescope.
Paper Summaries
For lectures with assigned readings (except for five lectures explicitly noted on the
schedule), every student will submit a paper summary for each assigned
paper on Gradescopeprior to the start of class. Paper summaries should
include Motivation, Novelty, Insights, FM Approach, Strengths, and
Critiques (see “Paper Presentations” for details).
Paper Presentations
For lectures with assigned readings (except for five lectures explicitly noted on the
schedule), 2-3 students will be assigned to present each paper and lead
the class discussion. Student presenters will spend ~10 minutes presenting
the assigned paper before leading the subsequent ~25 minute discussion.
Cover each of the following in your presentation, using the provided
Presentation Template:
Motivation: What key problem does the paper address? Why is it important?
Novelty: What is different about this work compared to prior work? Does the paper address a new problem, propose a new solution to an existing problem, or study an existing problem in a new context?
Insights: What key insights do the authors' key make towards addressing the problem?
Contributions: What are the key technical contributions of the paper?
FM Approach: What FM technique is deployed in the paper? How is the FM technique used? How are the system and problem formalized to take advantage of the FM technique?
Tool: Is there a tool? If so, what are its inputs and output, and how does it work?
Evaluation: How is the tool/solution evaluated?
Results: What are the key findings of the evaluation?
Strengths: What are the strengths of the authors' approach?
Critique: Is there anything you would change about the proposed solution or its implementation or evaluation?
Questions: Compile a list of questions to start the class discussion on the paper. Questions can involve things you wish the paper addressed better, broader implications of the paper, how you would extend the work (e.g., by changing the problem or solution, or using a different FM approach).
Project
You will carry out a quarter-long project, ideally in teams of 2-3 students.
You may use your existing research project if it is relevant to the course
and the instructor approves. But, there will have to be a piece of your
existing project that is explicitly carved out for the course project.
Please find a list of project ideas
here. Alternatively, you may devise a
completely original project. The course project deliverables include:
Project partners: 1/22/2026
Project proposal: 1/29/2026, 2-3 pages, 10pt font, single-spaced, single column
Midterm review: 2/20/2026, 3 slides maximum
Final presentation: 3/10/2026, ~15 minute talk
Final report: 3/17/2026, 5-6 pages, 10pt font, single-spaced, two-column
Artifact: 3/17/2026
Please find more details on the project deliverables
here.