Schedule subject to revision. Readings should be completed before class on the session listed. Homework is due before 6 a.m. on the date listed. Projects are due before midnight on the date listed. Homework and projects should be submitted by committing the required documents to your individual or team SVN repository. Unless otherwise specified, documents must be submitted in pdf format. See the syllabus for details on the late policy.
Schedule last updated Sun May 8.
Session quick links: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40
| Week | Session | HW Due 6am | Proj. Due 11:55pm | Reading | Quiz | Handout | Topic |
|---|---|---|---|---|---|---|---|
| 1 |
Mon Mar 7 |
Q1 | Introduction | ||||
| 1 |
Tue Mar 8 |
|
Q2 | What are formal methods? BRING LAPTOPS | |||
| 1 |
Thu Mar 10 |
HW1 (Solo) | No class, Curt covering 220 | ||||
| 1 |
Fri Mar 11 |
|
BRING LAPTOPS AND TEXT BOOK – Getting Started with Alloy | ||||
| 2 |
Mon Mar 14 |
|
Q3 | Logic of Alloy | |||
| 2 |
Tue Mar 15 |
|
Q4 | Alloy operators | |||
| 2 |
Thu Mar 17 |
Alloy Lab (Solo) |
|
Q5 | Alloy constraints | ||
| 2 |
Fri Mar 18 |
|
Q6 | Intro. to the Alloy modeling language | |||
| 3 |
Mon Mar 21 |
HW2 (Group) |
|
Q7 | Alloy fields and types | ||
| 3 |
Tue Mar 22 |
|
Q8 | Alloy paragraphs, examples | |||
| 3 |
Thu Mar 24 |
HW3 (Group) |
|
Q9 | Alloy commands and reuse | ||
| 3 |
Fri Mar 25 |
|
Q10 | Analysis | |||
| 4 |
Mon Mar 28 |
HW4 (Group) |
|
Q11 | Alloy examples | ||
| 4 |
Tue Mar 29 |
P1 | No class, project work day | ||||
| 4 |
Thu Mar 31 |
|
More Alloy examples | ||||
| 4 |
Fri Apr 1 |
HW5 (Solo) | Alloy Review | ||||
| 5 |
Mon Apr 4 |
HW6 (Group) | No class, project work day | ||||
| 5 |
Tue Apr 5 |
No class, project work day | |||||
| 5 |
Thu Apr 7 |
EXAM 1 (moved from session 18 to avoid conflict with CSSE 375) | |||||
| 5 |
Fri Apr 8 |
P2 | No class, project work day | ||||
| 6 |
Mon Apr 11 |
|
Q12 | Introduction to JML and Formal Verification | |||
| 6 |
Tue Apr 12 |
Q13 | More Program Verification—statements | ||||
| 6 |
Thu Apr 14 |
HW7 (Group) | Q14 | Program verification—notation | |||
| 6 |
Fri Apr 15 |
Catch up from convocation, then Optional program verification practice |
|||||
| 7 |
Mon Apr 25 |
|
Q15 | Program verification—methods | |||
| 7 |
Tue Apr 26 |
|
Q16 | Program verification—more methods | |||
| 7 |
Thu Apr 28 |
HW8 (Group) |
|
Q17 | Recursion, Data modeling with JML | ||
| 7 |
Fri Apr 29 |
Data modeling with JML (cont.) | |||||
| 8 |
Mon May 2 |
HW9 (Group) | No Q18 | Representation Hiding in JML | |||
| 8 |
Tue May 3 |
No class, project work day | |||||
| 8 |
Thu May 5 |
HW10 (Group) | Review | ||||
| 8 |
Fri May 6 |
EXAM 2 | |||||
| 9 |
Mon May 9 |
Q19 | State diagrams | ||||
| 9 |
Tue May 10 |
Q20 | Traffic Light | Statecharts | |||
| 9 |
Thu May 12 |
Q21 | Higher-order statecharts | ||||
| 9 |
Fri May 13 |
HW11 (Group) No Late Days! | No class, pick up Take-home EXAM 3 from my office before 4:30 p.m. (Exam due at start of class on Monday) | ||||
| 10 |
Mon May 16 |
|
Q22 | State of the practice in formal methods, course evaluations | |||
| 10 |
Tue May 17 |
No class, project work day | |||||
| 10 |
Thu May 19 |
HW12 (Solo) | No class, project work day | ||||
| 10 |
Fri May 20 |
P3 or P4 team's choice | No class, project work day |