# |
Date |
Prepare |
Exercises & Quizzes |
Topics |
Lab topic |
1 |
M 1/6 |
- |
- |
Surviving Formal Methods |
CS656/556 web site |
2 |
W 1/8 |
1.1+handouts |
Ex1.1 |
PC |
MATHS |
3 |
M 1/13 |
1.2+handouts |
Ex1.2 -1.6 |
Proofs |
MATHS |
4 |
W 1/15 |
1.3+handouts |
Ex1.7 |
Syntax |
XBNF |
- |
M 1/20 |
CSUSB |
HOLIDAY |
- |
- |
5 |
W 1/22 |
1.4+handouts |
Ex1.8-1.11 |
Semantics |
C++ bool |
6 |
M 1/27 |
1.5+handouts |
Ex1.12-1.15 |
Normal Forms |
cassert |
- |
M 1/27 |
LAST DAY |
TO DROP |
- |
- |
7 |
W 1/29 |
6.1+handouts |
Ex6.1-6.4 |
OBDDs |
OBDDs |
8 |
M 2/3 |
6.2+handouts |
Ex6.6-6.10 |
OBDDs |
OBDDs |
9 |
W 2/5 |
2.1,2.2,2.3+handouts |
Ex2.1-2.5 |
LPC |
Prolog |
10 |
M 2/10 |
2.4,2.5+handouts |
Ex2.5-2.8 |
LPC |
Prolog |
11 |
W 2/12 |
Review above |
Midterm on Logic |
- |
Semantic Tableaux |
12 |
M 2/17 |
3.1, 3.2+handouts |
Ex3.1-3.2 |
Model Checking |
State Machines? |
13 |
W 2/19 |
3.3, 3.4+handouts |
Ex3.3-3.4 |
CTL |
CTL on the WWW |
14 |
M 2/24 |
3.5, 3.6+handouts |
Ex3.7-3.9 |
SAT & SMV |
Using SMV |
15 |
W 2/26 |
6.3 not 6.3.4+handouts |
Ex 6.11-6.12 |
OBDDs in model checking |
Using SMV |
16 |
M 3/3 |
4.1, 4.2+handouts |
Ex4.1-4.2 |
Verification Framework |
SMV Source code |
17 |
W 3/5 |
4.3, 4.4+handouts |
Ex4.3-4.8 |
Partial Correctness |
Verification |
18 |
M 3/10 |
4.4+handouts |
Ex4.9 |
Total Correctness |
Verification? |
19 |
W 3/12 |
|
Presentations |
Hot Topics |
Hot Topics? |
20 |
M 3/17 |
|
Presentations |
Hot Topics |
Hot Topics? |
Final |
F 3/21 |
Chs 1,2,3,4,6, etc |
|
Comprehensive |
|
9am |
T 3/25 |
Grades WWW |
* draft grade posted earlier. |
|
|