Schedule
Note: this schedule is tentative and may change based on student feedback as the semester progresses.
| Day | Content | Reading | Due |
|---|---|---|---|
| Wed, Jan 22 | |||
| Thu, Jan 23 |
Economics of Software Correctness
David R. MacIver, 2016. |
||
| Mon, Jan 27 |
The Fuzzing Book: Introduction to Software Testing
Skim through `Run-Time Verification`. Zeller et al, 2024. |
||
| Wed, Jan 29 |
Workshop: Launch PBT
|
Due: Preliminaries (Gradescope)
|
|
| Thu, Jan 30 |
Property-Based Testing in Practice
Harrison Goldstein et al, 2024. Feel free to read before or after class, we will discuss Monday the 3rd |
||
| Mon, Feb 3 |
Evaluating the “Small Scope Hypothesis”
Read Abstract, skim Introduction. Andoni et al, 2002. |
||
| Wed, Feb 5 |
Workshop: Launch Modeling 1
|
Skim book: Ch. 1-2.5 | |
| Thu, Feb 6 | Skim book: Ch. 3.0-3.2.3 |
Due: PBT
|
|
| Mon, Feb 10 | Skim book: Ch. 3.4, read 3.5.1-3.5.2 | ||
| Wed, Feb 12 |
Workshop: Launch Modeling 2
|
Due: Modeling 1
|
|
| Thu, Feb 13 |
AlloyDocs: Time
Hillel Wayne, 2024. |
||
| Mon, Feb 17 | Presidents' Day; no class | ||
| Tue, Feb 18 |
(Optional/supplemental): Alloy 6: It's about time blog post
Hillel Wayne, 2021. |
||
| Wed, Feb 19 |
Workshop: Launch Modeling 3
|
Due: Modeling 2
|
|
| Thu, Feb 20 |
(Discussion): The Urgent Need for Memory Safety in Software Products
Press release from the US Cybersecurity Agency, 2023 |
||
| Mon, Feb 24 |
(Supplemental): Automated Memory Management
Wikipedia |
||
| Wed, Feb 26 |
Workshop: Launch Modeling 4
|
Due: Modeling 3
|
|
| Thu, Feb 27 | |||
| Mon, Mar 3 |
(Supplemental): Peterson's algorithm
Wikipedia |
||
| Wed, Mar 5 |
Workshop: Catchup day; finish modeling 4
|
Due: Modeling 4
|
|
| Thu, Mar 7 |
(Supplemental): Formally Modeling Database Migrations
Hillel Wayne, 2019 |
||
| Mon, Mar 10 |
Boolean Satisfiability: From Theoretical Hardness to Practical Success
Malik & Zhang, 2009 |
||
| Wed, Mar 12 |
Workshop: Working session for Modeling 5
|
||
| Thu, Mar 13 | |||
| Mon, Mar 17 | Spring break | ||
| Mon, Mar 24 | |||
| Wed, Mar 26 |
Workshop: Launch SAT
|
Due: Modeling 5
|
|
| Thu, Mar 27 |
Why Amazon Chose TLA+
Chris Newcombe, 2014 |
||
| Mon, Mar 31 |
(Supplemental): SAT/SMT by Example
Dennis Yurichev, 2024 |
||
| Wed, Apr 2 |
Workshop: Launch SMT 1
|
Due: Solver
|
|
| Thu, Apr 3 | |||
| Mon, Apr 7 |
(Supplemental): Symbolic execution and program testing
James C. King, 1976 |
||
| Wed, Apr 9 |
Workshop: Final project group formation
|
Due: SMT 1
|
|
| Thu, Apr 10 |
The Coming Software Apocalypse
James Somers for The Atlantic, 2017 |
||
| Mon, Apr 14 |
Workshop: Launch SMT 2
|
||
| Wed, Apr 16 | Ruhlman conference; no class | ||
| Thu, Apr 17 |
Program synthesis
|
Due: Final project proposal
|
|
| Mon, Apr 21 | Patriots day; no class | ||
| Wed, Apr 23 |
Workshop: Final project checkins
|
Due: SMT 2
|
|
| Thu, Apr 24 |
Guest lecture: Anjali Pal, University of Washington
|
||
| Mon, Apr 28 |
Final project checkins
|
||
| Weds, Apr 30 |
No workshop
|
||
| Thu, May 1 |
Final class! Guest lecture: Carolyn Zech, AWS
|
||
| Mon, May 6 | Final exam period starts | ||
| Thurs, May 8 | Final exam period |
Due: Final presentations, 9-11:30am
|
|
| Fri, May 9 |
|
Due: Final project code, report
|