CS 257: Introduction to Automated Reasoning

Autumn 2023, Mon/Wed 10:30 AM PDT - 11:50 AM PDT, Jen-Hsun Huang Engineering Center 18

Faculty Instructor: Caroline Trippel
Student Instructor: Andrew (Haoze) Wu
Teaching Assistant: Hanna Lachnitt

Syllabus: Syllabus
Canvas: Class Homepage
Ed Discussion : Ask a Question on Ed

Automated logical reasoning has enabled substantial progress in many fields, including hardware and software verification, theorem-proving, and artificial intelligence. Different application scenarios may require different automated reasoning techniques and sometimes their combination. In this course, we will study the theory and practice of automated reasoning. We start with propositional logic and the propositional satisfiability (SAT) problem. We then move on to general first-order reasoning, including first-order resolution and unification. We next consider first-order theories, such as linear arithmetic over reals and integers, uninterpreted functions, bit-vectors, and arrays. We cover the satisfiability modulo theories (SMT) problem, the DPLL(T) calculus for SMT, and techniques for reasoning about combinations of theories. The course will include many examples of practical applications of these algorithms as well as guest speakers who will tell us about their use in industry.

Overview

Units This class is offered for 3 units as either a letter grade or a CR/NC course.

Prerequisites CS154 Introduction to the Theory of Computation, or CS106B Programming Abstractions and CS103 Mathematical Foundations of Computing, or consent of instructor.

Learning Objectives Through active engagement and completion of course activities, you will be able to:

Understand the syntax, semantics, and properties of different logical languages for encoding different decision problems;
Understand and prove properties about popular automated reasoning procedures (e.g., CDCL, DPLL(T), Simplex, Nelson-Oppen);
Get hands-on experience in using off-the-shelf automated reasoning tools;
Understand the roles of automated reasoning in real-world applications such as software/hardware verification and synthesis;
Get exposure to formal methods literature and engage in formal methods research.

Commitment to Inclusion

We are committed to creating a respectful, welcoming, and inclusive environment where students from all backgrounds and perspectives are well-served. To achieve this goal, we encourage all members of the class to conduct discussions in or out of class in a way that shows respect and dignity to everyone. We value your thoughts and encourage you to communicate them while allowing others to express their thoughts as well. This will allow for rigorous intellectual engagement and a deeper learning experience for all. We appreciate your suggestions on ways to improve the effectiveness of the course for you personally or for other students. If any of our class meetings conflict with your religious events, please let us know so that we can make arrangements for you.

Schedule

Date	Topic	Lecturer	Supplemental Reading	Class Notes
9/27	Propositional Logic: Syntax, semantics, satisfiability and validity	Caroline Trippel	CC 1.1-1.5 MI 1.0-1.2	Slides
10/02	Proof Systems	Guest lecture by Clark Barrett, Stanford University	Book Chapter	Slides
10/04	Propositional Logic: Normal forms, SAT, resolution, DPLL	Caroline Trippel	CC 1.6-1.7 MI 1.6	Slides
10/09	Propositional Logic: Abstract DPLL, CDCL	Caroline Trippel	DP Chapter 2	Slides
10/11	CDCL	Caroline Trippel		Slides
10/15
10/16	First-order logic: syntax	Andrew Wu	MI 2.1, MI 2.2 before "Definability in a Structure"	Slides
10/18	First-order Logic: Semantics, clausal forms	Andrew Wu	CC Ch. 2.1-2.6	Slides
10/20
10/23	SMT: Overview on Theories	Hanna Lachnitt	CC Ch. 3 (After class)	Slides
10/25	Applications: Model Checking	Caroline Trippel
10/30	Applications: Formal Explanation of AI	Guest lecture by Nina Narodytska, VMware		Slides
10/31	Halloween midterm review session with cookies!
11/01	SMT: Decision procedures for strings and sequences	Guest lecture by Clark Barrett, Stanford University		Slides
11/02
11/04
11/06	SMT: DPLL(T)	Andrew Wu	DP Ch. 3	Slides
11/08	SMT: Arithmetic	Andrew Wu	DP Ch 5.1-5.2	Slides
11/13	SMT: Bit-vectors	Guest lecture by Mathias Preiner, Stanford University	DP Ch 6
11/15	Application: Symbolic Execution	Caroline Trippel
11/17	Course withdrawal deadline
11/20	Thanksgiving Recess (no classes)
11/22	Thanksgiving Recess (no classes)
11/27	AI for AR	Guest lecture by Christopher Hahn, Google		Slides
11/29	SMT: Herbrand's theorem, quantifier instantiation	Andrew Wu	DP Ch. 9.5	Slides
12/04	SMT: Theory combination	Caroline Trippel	DP 10.1-10.5	Slides
12/06	Hardware Security Verification	Guest lecture by John Matthews, Intel
12/12

Course Materials

Ed Discussion Ed Discussion (https://edstem.org/us/courses/44522 ) will be used both for online discussion and for announcements. We recommend keeping email notifications on from Ed Discussion (https://edstem.org/us/settings/) to avoid missing any time-sensitive announcements.

Canvas Recordings of the lectures and additional supplementary materials will be available on Canvas ( https://canvas.stanford.edu/courses/176963 ).

Poll Everywhere We will use Poll Everywhere to facilitate in-class discussions and quizzes.

Technology You will need to have access to a PC to complete the programming components of homework assignments. You will also need internet connection so that you can access email, class website, Ed discussion, and Canvas. Students can borrow equipment and access other learning technology from the Lathrop Learning Hub

Readings Reading assignments for each lecture will be posted at least 1 week in advance. You are expected to have read those materials before the lecture. The readings will be primarily selected from the following textbooks accessible through your Stanford account:

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).
MI: A Mathematical Introduction to Logic by Herbert B. Enderton (online version).

For more recent topics, papers will be assigned.

Office Hours

*Office hours by appointment after the week of Dec. 4

Caroline: Wednesdays (12pm-1pm) in Gates 470;
Andrew: Tuesdays (9am-10pm) in Gates 498;
Hanna: Mondays (2pm-3pm) in Gates 104 and Thursdays (3pm-4pm) in room Gates 498.

If you cannot make these hours or need to join virtually please reach out directly to the course staff member you intend to meet.

Deliverables

Homework

There will be 3 written homework assignments given in the first half of the quarter. The assignments contain problem sets that evaluate your understanding of the concepts and proof techniques covered in class and the reading. Two of the assignments also have programming components, where you will gain experience on using automated reasoning tools. Homework will be due before class (10:00 AM) and submitted on Canvas. Please do not email your homework to the course staff unless asked. Solutions will be available online shortly after the deadline once every student has submitted their solution.

Assignment 1, released 10/2, due Wednesday 10/11
Assignment 2, released 10/11, due Friday 10/20
Assignment 3, released 10/20, due Monday 10/30

Midterm

There will be one take-home midterm exam, which will contain problems similar in style to the homework assignments. Preparing for the exam will enable you to reinforce your understanding of the key concepts and proof techniques covered in the first half of the quarter. It will cover lectures 1 through 8 (except for lecture 5). The take-home midterm will be released on Thursday, Nov. 2, at 7:00 AM. It will be available for 48 hours until Saturday, Nov. 4 at 7:00 AM. The exam is expected to take 2 hours. A room on campus will be provided for those who wish to take the exam there. We ask that you take the exam at home if you are able as the reserved room will likely not be large enough to accommodate everyone. There will be a 1 hour review session on Tuesday, Oct. 31, from 10:30 AM to 12:00 PM in Gates B12, where students will have the opportunity to ask questions.

Final Project

You will carry out a course project in the second half of the quarter. You are expected to work in teams of two, but may choose to work individually in special circumstances with permission from the course staff. You have two options for the course project:

Option 1: Implement a decision procedure and an optimization of it. Present an experimental evaluation of your implementation. For example, the decision procedure could be the DPLL procedure, the optimization could be watched literals, and the evaluation could be (subsets of) benchmarks from the recent SAT competition.

Option 2: Work on a research problem related to automated reasoning. Suitable projects include improving an existing automated reasoning technique, or applying automated reasoning techniques to solve a domain-specific challenge.

You are encouraged to consult with an instructor to determine if your project is adequate for the course. The deliverables of the course project include:

a 1-page project proposal summarizing your selected project direction and goals, explaining your proposed deliverables and plan of work, and outlining a plan for experimental evaluation. Due date: 11/06/23
a 4-5 page project report detailing your selected project direction and goal, explaining your methods and completed work, presenting experimental evaluation, and summarizing your findings. Due date: 12/12/23
Code or proof artifact so that the course staff may reproduce your experimental results and understand your methods in detail. Due date 12/12/23

Course Policies

Grades

Category	Grades %	Notes
Attendance and participation in class	15%	3 conditional absence "passes" (see below) Arrival/departure > 10 min late/early counts as an absence
Homework	40%	Eligible for late days One can be revised for extra credit
Midterm	20%	Not eligible for late days Can be revised for extra credit
Final Project	25%	Only project proposal is eligible for late days

Attendance

Non-SCPD student gets 3 “passes” to be physically absent from class without losing participation points, provided that you:

watch the recording; and
complete and submit the in-class exercises within a week.

Arriving/departing >10 minutes late/early to/from a class counts as an absence.
We understand circumstances may arise that will interfere with your ability to attend class, such as feeling sick or needing to quarantine for the safety of everyone. In light of these considerations, we request that you:

skip class if you are feeling sick, especially if you have any COVID-19 symptoms;
watch the lecture recording posted on Canvas;
complete the in-class quiz asynchronously;
remember that you have 3 absence “passes”;
meet with the course staff afterwards to ask questions and get caught up.

If you have already used up all late “passes” and are sick, please contact the course staff. Please do not come to class if you are ill! Our priority is to keep everyone healthy while maximizing your learning in this course.

Other Logistics

Collaboration: You are encouraged to discuss assignments with other students. However, each student must independently write their own solution to homework assignments. Submitting solutions or code written by another person is a violation of the Honor Code. See: honor code and collaboration for some general guidelines, which apply to both project assignments and problem sets.

Accommodations: Students who may need an academic accommodation based on the impact of a disability must initiate the request with the Office of Accessible Education (OAE). Professional staff will evaluate the request with required documentation, recommend reasonable accommodations, and prepare an Accommodation Letter for faculty dated in the current quarter in which the request is being made. Students should contact the OAE as soon as possible since timely notice is needed to coordinate accommodations. The OAE is located at 563 Salvatierra Walk; phone: 723-1066; web site http://studentaffairs.stanford.edu/oae.