Schedule
Note: this schedule is tentative and may change based on student feedback as the semester progresses.
| Day | Content | Reading | Due |
|---|---|---|---|
| Mon, Jan 22 | |||
| Wed, Jan 24 |
Workshop: Launch Preliminaries
|
||
| Thu, Jan 25 |
Economics of Software Correctness
David R. MacIver, 2016. |
||
| Mon, Jan 29 |
The Fuzzing Book: Introduction to Software Testing
Skim through `Run-Time Verification`. Zeller et al, 2024. |
||
| Tue, Jan 30 |
|
Due: Preliminaries
|
|
| Wed, Jan 31 |
Workshop: Launch PBT
|
||
| Thu, Feb 1 |
Evaluating the “Small Scope Hypothesis”
Read Abstract, skim Introduction. Andoni et al, 2002. |
||
| Mon, Feb 5 | Read book: Ch. 1 | ||
| Tue, Feb 6 |
|
Due: PBT
|
|
| Wed, Feb 7 |
Workshop: Launch Modeling 1
|
Skim book: Ch. 2.0-2.5 | |
| Thu, Feb 8 | Skim book: Ch. 3.0-3.2.3 | ||
| Mon, Feb 12 | Skim book: Ch. 3.4, read 3.5.1-3.5.2 | ||
| Tue, Feb 13 |
|
Due: Modeling 1
|
|
| Wed, Feb 14 |
Workshop: Launch Modeling 2
|
||
| Thu, Feb 15 |
AlloyDocs: Time
Hillel Wayne, 2024. |
||
| Mon, Feb 19 | Presidents' Day; no class | ||
| Tue, Feb 20 |
(Optional/supplemental): Alloy 6: It's about time blog post
Hillel Wayne, 2021. |
||
| Wed, Feb 21 |
Workshop: Launch Modeling 3
|
||
| Thu, Feb 22 |
(Optional/supplemental): The Urgent Need for Memory Safety in Software Products
Press release from the US Cybersecurity Agency, 2023 |
Due: (Extended) Modeling 2
|
|
| Mon, Feb 26 |
(Supplemental): Automated Memory Management
Wikipedia |
||
| Tue, Feb 27 |
|
Due: Modeling 3
|
|
| Wed, Feb 28 |
Workshop: Launch Modeling 4
|
||
| Thu, Feb 29 | |||
| Mon, Mar 4 | |||
| Tue, Mar 5 |
|
Due: Modeling 4
|
|
| Wed, Mar 6 |
Workshop: Launch Modeling 5
|
||
| Thu, Mar 7 |
(Supplemental): Peterson's algorithm
Wikipedia |
||
| Mon, Mar 11 |
(Supplemental): Formally Modeling Database Migrations
Hillel Wayne, 2019 |
||
| Tue, Mar 12 |
|
||
| Wed, Mar 13 |
Workshop: Catch up day; finish modeling 5
|
Due: Modeling 5
|
|
| Thu, Mar 14 |
Why Amazon Chose TLA+
Chris Newcombe, 2014 |
||
| Mon, Mar 18 | Spring break | ||
| Mon, Mar 25 | |||
| Wed, Mar 27 |
Workshop: Launch Solver
|
||
| Thu, Mar 28 |
(Supplemental): SAT/SMT by Example
Dennis Yurichev, 2024 |
||
| Mon, Apr 1 |
Boolean Satisfiability: From Theoretical Hardness to Practical Success
Malik & Zhang, 2009 (Supplemental): SAT/SMT by Example Dennis Yurichev, 2024 |
||
| Tue, Apr 2 |
|
Due: Solver
|
|
| Wed, Apr 3 |
Workshop: Launch SMT 1
|
||
| Thu, Apr 4 | |||
| Mon, Apr 8 |
(Supplemental): Symbolic execution and program testing
James C. King, 1976 |
||
| Tue, Apr 9 |
|
Due: SMT 1
|
|
| Wed, Apr 10 |
Workshop: Final project group formation
|
||
| Thu, Apr 11 | Ruhlman conference; no class | ||
| Mon, Apr 15 | Patriots day; no class | ||
| Tue, Apr 16 |
|
||
| Wed, Apr 17 |
Workshop: Launch SMT 2
|
||
| Thu, Apr 18 |
Cranelift project description
Bytecode Alliance, 2024 (Supplemental): Bringing the web up to speed with WebAssembly Haas et al, 2017 (Supplemental): Efficient software-based fault isolation Wahbe et al, 1993 |
Due: Final project proposal
|
|
| Mon, Apr 22 |
(Supplemental): SIGPLAN Blog, Fast and Extensible Equality Saturation with egg
Max Willsey, 2021 |
||
| Tue, Apr 23 |
|
Due: SMT 2
|
|
| Wed, Apr 24 |
Workshop: Final project checkins
|
||
| Thu, Apr 25 |
Program synthesis, outlook
|
||
| Mon, Apr 29 |
Project checkins on Zoom
|
||
| Weds, May 1 |
Project checkins on Zoom
|
||
| Mon, May 6 | Final exam period | ||
| Tues, May 7 | 9-11:30 AM: Student final project presentations | ||
| Weds, May 8 | Final exam period |
Due: Final project code, report
|