Tentative Schedule for CMSC 433
Fall 2023 |
|
|
|
|
|
|
|
|
| Date |
# |
Topic |
|
Assignments |
|
|
|
|
|
|
|
| Tue 08-29 |
1 |
Introduction; propositional calculus |
|
|
|
| Thu 08-31 |
2 |
Formal proofs for the propositional calculus: Sequent calculus |
|
HW1 out 09-01 |
|
| Tue 09-05 |
3 |
Predicate calculus |
|
|
|
| Thu 09-07 |
4 |
Sequent calculus proofs for the predicate calculus |
|
HW1 due / P0 out 09-08 |
| Tue 09-12 |
5 |
Programming in Dafny |
|
|
|
| Thu 09-14 |
6 |
Specifications:
preconditions, postconditions, annotations |
|
P0 due / P1 out 09-15 |
| Tue 09-19 |
7 |
Using annotations in Dafny |
|
|
|
| Thu 09-21 |
8 |
Loop invariants |
|
|
|
| Tue 09-26 |
9 |
Termination |
|
|
|
| Thu 09-28 |
10 |
DISTINGUISHED LECTURE:
Bratin Saha, VP of AI/ML at Amazon |
|
P1 due 09-29 |
|
| Tue 10-03 |
11 |
Using Dafny:
inference in Dafny |
|
|
|
| Thu 10-05 |
12 |
Using Dafny:
specification infrastructure |
|
P2 out 10-06 |
|
| Tue 10-10 |
13 |
Using Dafny: tips
and tricks |
|
|
|
| Thu 10-12 |
14 |
MIDTERM |
|
|
|
| Tue 10-17 |
15 |
Programming in Haskell |
|
|
|
| Thu 10-19 |
16 |
Programming in Haskell (cont.) |
|
P2 due / P3 out 10-20 |
| Tue 10-24 |
17 |
Types as specifications |
|
|
|
| Thu 10-26 |
18 |
Liquid types in Haskell |
|
|
|
| Tue 10-31 |
19 |
Liquid types in Haskell (cont.) |
|
|
|
| Thu 11-02 |
20 |
Using Liquid Haskell |
|
P3 due / P4 out 11-03 |
| Tue 11-07 |
21 |
Using Liquid Haskell (cont.) |
|
|
|
| Thu 11-09 |
22 |
Inference in Liquid Haskell |
|
|
|
| Tue 11-14 |
23 |
SAT solving |
|
|
|
| Thu 11-16 |
24 |
Using SAT solvers |
|
P4 due / P5 out 11-17 |
| Tue 11-21 |
25 |
SMT solving |
|
|
|
| Thu 11-23 |
|
THANKSGIVING |
|
|
|
| Tue 11-28 |
26 |
Using SMT solvers |
|
|
|
| Thu 11-30 |
27 |
Foundations of Dafny:
Hoare Logic and SMT |
|
|
|
| Tue 12-05 |
28 |
Foundations of Liquid Haskell: Constructive type theory and SMT |
|
|
|
| Thu 12-07 |
29 |
Exam review |
|
P5 due 12-08 |
|
|
|
|
|
|
|
| Tue 12-12 |
|
READING DAY |
|
|
|
| Tue 12-19 |
|
FINAL EXAM (10:30 -- 12:30) |
|
|
|
|
|
|
|
|
|
| UMD
Web Accessibility |
|
|
|
|
|
|
|
|
|