Watch this space for the latest updates.
The class mailing list is compsci703-1-f23@g-groups.wisc.edu. An archive of mail sent to the class can be found here.
Last updated: 5:56 PM, Monday, December 8, 2023
Meeting Times and Location
Mondays, Wednesdays, and Fridays, 2:30 PM - 3:45 PM, on the days indicated in the
course schedule, in 1240 CS.
On September 15 and October 20, there are conflicting events in 1240 CS, so we wil meet on
Zoom.
Depending on the Covid situation, other classes may be broadcast on that link, too.
Credits
3
How the Course Meets the Credit-Hour-Policy Standards
Modified ``3-Credit Course, Option B'':
The classroom is reserved for three 75-minute class periods each week over the
semester;
however, on average we will meet for two 75-minute class periods per week.
Until late October, we will front-load the classes and meet for three
75-minute class periods most weeks, after which there will be no
classes, and you will have five uninterrupted weeks to work on a
project of your own choosing.
In the final week of the term, we will hold enough classes for each project-group to make
an 18-minute presentation about the work they carried out.
See the course schedule for the dates on which
classes will be held.
The class carries the expectation that, on average, students will work on course learning activities (reading, writing, problem sets, projects, etc.) for about 3 hours out of the classroom for every class period.
More information about the expectations for student work can be found elsewhere on this page.
Instructional Mode
Lecture by the instructor, and at the end of the term, a short project presentation by each project-group.
UW Policies
The course will be conducted in conformance with the UW policies found on the page at
this link.
In particular, policies about accommodating religious observances are detailed at
this link.
Please note that ``students are responsible for notifying instructors within the first two weeks of classes of the date(s) when they request relief due to a religious observance.''
Instructor
Professor Thomas Reps
Office: 6361 Computer Sciences
Office hours: By appointment, typically on Zoom
E-mail: reps at cs.wisc.edu
Home page: www.cs.wisc.edu/~reps/
Textbook and Notes
There is no required textbook for the course.
Much of the reading material for the course is available on-line;
see the course bibliography.
There are on-line notes for some of the topics we will cover in this directory. The relevant notes cover the following topics:
Over the course of the semester, we will accumulate a set of PowerPoint slides that will be posted in the Course Schedule.
and possibly other topics as time permits.
Assignments
There may be a few problem sets (2-3), possibly a paper critique or two, and a course project.
The bulk of the coursework will be the project.
Course Project
For the course project, you will work on a problem with a partner.
The first step is to find a partner and write a project proposal (1-2 pages) that describes
the following items:
So that you have an idea of the scope of an appropriate project, here are the abstracts of the presentations from the Fall 2015 version of a related course: Fall 2015 CS 701 abstracts.
To help keep you on track, I will impose five deadlines:
I may be looking for a few volunteers to prepare LaTeX notes for one
or more of the term's classes -- more about this topic later in the
semester.
Students who do such a task may receive extra credit.
Policy on Collaborative Work
A certain amount of discussion of problem sets is permitted.
You should not ``go to someone,'' nor Google, nor ChatGPT simply to get an answer;
the kind of collaboration intended is a discussion with someone else
in which you discover the answer jointly.
You are not to make a habit of it over the course of the semester.
(Points will be deducted if you do an excessive amount
of the course work in collaboration with other people.)
When you do work in collaboration with someone else, make a note of it on the solution set that you turn in. In all cases, you are to do your own write-up.
For the end-of-course project, you are encouraged to work in groups of two.
Topics to be covered include logic, verification, SAT solving, abstract interpretation, static-analysis path problems, and program synthesis, including algorithms relevant to those topics. A smattering of other topics will be covered, such as semantics, some type theory, and material both related to -- and relevant for -- machine learning.
It is useful, but not mandatory, for students to have completed an undergraduate compiler course, such as Wisconsin's CS 536.
Note: we are not interested in flaws in presentation, such as trivial examples, confusing notation, or spelling errors. However, if you have a great idea on how some concept could be presented or formalized better, mention it.
What follows is a tentative schedule of topics:
DATE TOPIC READINGS PURPOSE
=====================================================================================================
9/6 Introduction; course mechanics PPT Slides Introduction
9/8 Overview of six formalisms for semantics [Nielson & Nielson 1999] Background
PPT Slides
-----------------------------------------------------------------------------------------------------
9/11 First-order logic, axiomatic semantics, [Hoare 1969] Background
verification conditions PPT Slides
9/13 Weakest preconditions, strongest Background
postconditions, symbolic execution PPT Slides
9/15 ZOOM CLASS (Event occurring in 1240 CS) Lecture Notes Background
Static program analysis PPT Slides
Recording, Part I
Recording, Part II
-----------------------------------------------------------------------------------------------------
9/18 Intro to abstract interpretation; [Cousot & Cousot 1977] Background
lattices and fix-points of equations PPT Slides
on lattice elements
9/20 Automating abstract interpretation via [R., Sagiv, & Yorsh 2004] Synthesis in service of analysis
the strongest-consequence problem PPT Slides
9/22 Introduction to program synthesis [Gulwani 2010] Synthesis
(Guest lecturer: Loris D'Antoni) [D'Antoni and Polikarpova 2022]
PPT Slides
-----------------------------------------------------------------------------------------------------
9/25 Automating abstract interpretation [Thakur & R. 2012] Synthesis in service of analysis
+ refutation as lattice search PPT Slides + abs. int. in service of verification
9/27 Propositions as types [Wadler 2015] Synthesis
PPT Slides
9/29 CDCL SAT solving [Marques-Silva et al. 2008], Verification
(also [Tichy & Glase 2006],
[Mitchell 2005],
and [Eén and Sörensson 2003])
PPT Slides
---------------------------------------------------------------------------------------------------------
10/2 What is a path problem? Lecture Notes Program analysis
PPT Slides
10/4 Automatic differentiation Lecture Notes Interlude: ML
and back-propagation [Olah 2015]
PPT Slides
10/6 Collecting semantics as a path problem Lecture Notes Program analysis
PPT Slides
----------------------------------------------------------------------------------------------------
10/9 Abstract semantics as a path problem Lecture Notes Program analysis
PPT Slides
10/11 Functional approach to interprocedural Lecture Notes, Part I Program analysis
dataflow analysis Lecture Notes, Part II
[Sharir & Pnueli 81]
PPT Slides
10/13 Program analysis via CFL-reachability [Reps 1998] Program analysis
[RHS 1995]
PPT Slides
-----------------------------------------------------------------------------------------------------
10/16 Weighted pushdown systems [RLK 2007] Program analysis
PPT Slides about points-to analysis via CFL-reachability
PPT Slides about WPDSs
10/18 Synthesis with hard + soft constraints [KMDRR 2022] Synthesis in service of analysis
(Kanghee Park, guest lecturer) [Park et al. 2023]
PPT Slides
10/20 ZOOM CLASS (Event occurring in 1240 CS)
A few topics about synthesis: Synthesis
(i) CEGIS [Solar-Lezama et al. 2008, Sect. 5.1]
(ii) E-graphs, tree automata, and blog, [Wang et al. 2021], slides, [Koppel 2021]
version-space algebra [Polozov and Gulwani 2015, Sect. 4]
PPT Slides
------------------------------------------------------------------------------------------------
10/23 Counter-example-guided abstraction [Ball & Rajamani 2000] Program analysis via synthesis for abstraction refinement
refinement (CEGAR) [Ball & Rajamani 2001a,2001b]
PPT Slides
10/25 Analysis of concurrent programs [Farzan & Kincaid 2012] Program analysis
[Farzan & Kincaid 2013]
PPT Slides
10/27 Newtonian program analysis Lecture Notes Program analysis
[RTP16], [RTP17]
PPT Slides
10/27 Project proposal due (5:15 PM)
------------------------------------------------------------------------------------------------
10/30 Tips on writing a research paper PPT Slides Writing
11/1 No class
11/3 Retrograde debugging Page with links to the video recording
PPT Slides
------------------------------------------------------------------------------------------------
11/6 No class
11/8 No class
11/10 No class
11/10 Milestone 1 due (5:15 PM)
------------------------------------------------------------------------------------------------
11/13 No class
11/15 No class
11/17 No class
------------------------------------------------------------------------------------------------
11/20 No class
11/22 No class
11/22 Milestone 2 due (5:15 PM)
11/23-11/26 Thanksgiving Break
------------------------------------------------------------------------------------------------
11/27 No class
11/29 No class
12/1 No class
12/3 Presentation abstract due (5:15 PM)
------------------------------------------------------------------------------------------------
12/4 No class
12/6 FINAL PROJECT PRESENTATIONS
12/8 FINAL PROJECT PRESENTATIONS
------------------------------------------------------------------------------------------------
12/11 FINAL PROJECT PRESENTATIONS
12/13 FINAL PROJECT PRESENTATIONS
12/15 FINAL PROJECT WRITEUPS DUE (5:15 PM, as a PDF file, by e-mail to reps at cs.wisc.edu)
------------------------------------------------------------------------------------------------