Date

Meeting

Topic

Lecturer

Lab / Homework

Reading

9/4

1 T

Introduction to Analysis and Artifacts

J

Lab#1
(req) out

[BB]

9/6

2 R

Requirements Analysis: Formalization

J



9/11

3 T

Design Analysis I: highlevel

J



9/13

4 R

Presentation of Lab#1

S

Lab#2
(travel) out, Project out

[Bloom]

9/18

5 T

Design Analysis II: lowlevel

J


[Wing87,Wing88,Wing96]

9/20

6 R

Presentation of Lab#2

S

Lab#3
(C string) out


9/25

7 T

No class / Guest




9/27

8 R

Presentation of Lab #3

S



10/1


Makeup class: Please
attend Peter
Ryan's talk 3:30 p.m. 5409 WeH




10/2

9 T

Interface Analysis: Lab#4
(switch) inclass

J, S



10/4

10 R

No class / Guest




10/9

11 T

Performance
Analysis: queueing theory
(.pdf
version)

J

HW
out

[Jain0,
Jain
1]

10/11

12 R

Performance
Analysis: stochastic models
(.pdf
version)

J

Lab#4
write up due

[Jain
2]

10/16

13 T

Code
Analysis: Verification

J


[Gries,
HJ1, HJ2]

10/18

14 R

Code
Analysis: Slicing
(.pdf
version)

J


[Binkley]

10/23

15 T

Code
Analysis: Tools
(.pdf
version)

O'Brien



10/25

16 R

Model
Checking: STS, CTL
(.pdf
version)

J

Lab#5
(temporal logic, C code) out






HW due

[CGP]

10/30

17 T

Model Checking: symbolic
(BDD), explicit

J



11/1

18 R

Model Checking: SMV
(.pdf
version)

Chauhan



11/6

19 T

Model Checking: state reduction
techniques

J



11/8

20 R

Presentation of Lab#5

S

Lab#6
(switch, again) out


11/13

21 T

Protocol Analysis: Lab#7
(AFS) inclass

J

Lab#7

[Satya]

11/15

22 R

Security
Analysis: authentication logic

J

Lab#6
write up due

[BAN]

11/20

23 T

Reengineering

O'Brien


[SM]

11/22

R

No Classes (Thanksgiving)




11/27

24 T

Presentation of Lab#7

S



11/29

25 R

Security
Analysis: protocol analysis

J


[KMM]

12/4

26 T

Survivability
Analysis

Mead


[E99,
ELTM]

12/6

27 R

Presentation of Project

S

Project write up due


12/11

28 T

Presentation of Project

S


