Date
|
Topic
|
Slides
|
Participation
|
Reading
|
Assignment
Due (10:30am)
|
Introduction
|
Jan 12
|
Course
Overview; Orthogonal Defect Classification
|
1-course-intro.pdf
|
|
Orthogonal Defect
Classification--A Concept for In-Process Measurements
|
|
| Traditional Analysis: Testing and Inspection |
| Jan 14 |
Inspection |
2-inspection.pdf
|
|
Wiegers text (optional) |
|
Jan 19
|
Testing 1
|
3-testing.pdf
|
Lect03.doc
|
What is software testing? And why is it so
hard? |
10:30am: Assignment 1: Specification
Inspection and Java
|
| Jan 21 |
Testing 2
|
4-testing.pdf
|
Lect04.doc
|
Kaner
text (optional)
|
|
| Design Analysis: Patterns and Frameworks |
Jan 26
|
Design Patterns
|
5-patterns.pdf
|
|
Shalloway text (required)
|
|
Jan 28
|
Patterns and Frameworks
|
(same)
|
Patterns in Conway's Game of
Life (code
and model
from Allen Holub's book)
|
Frameworks =
Components + Patterns
|
10:30am: Assignment 2: Code Inspection
and Testing; Hnefatafl rules
|
Feb 2
|
Testing Discussion |
7-testing.pdf
|
|
|
|
Feb 3
|
|
|
|
|
5pm: Assignment 3: Design Pattern
Mining
|
Feb 4
|
Pattern Examples and Frameworks |
8-frameworks.pdf;
pattern-examples.zip
(6 MB)
|
|
|
|
| Program Specification and Verification |
Feb 9
|
Hoare Logic: Reasoning about
Correctness |
9-hoare.pdf
|
Lect09.doc
|
3-hoare-notes.pdf;
3-hoare.tex; An Axiomatic
Basis for Computer Programming |
|
| Feb 11 |
Hoare Logic (continued)
|
10-hoare.pdf
|
Lect10.doc
|
Huth text (optional) |
|
Feb 12
|
|
|
|
|
5pm: Assignment 4: Framework Design |
| Feb 16 |
ESC/Java: Code Verification |
11-escjava.pdf
|
|
Extended Static
Checking for Java;
Multiply.java; Multiply-full.java; SimpleSet.java; SimpleSet-full.java |
|
Feb 17
|
|
|
|
|
10:30am: Assignment 5: Design
Inspection |
| Feb 18 |
Plural: Protocol Checking |
12-plural.pdf
|
Papers on Plural theory
and experience
|
|
|
| Feb 23 |
Plural, continued
|
13-plural.pdf
|
Plural implementation and
additional information |
|
|
| Feb 25 |
Framework Design Presentations |
|
|
|
10:00am: Assignment 6: Hoare
Logic, ESC/Java, and Design Presentation; Stack.java; StackCheck.java |
Mar 2
|
Framework Design Presentations
|
15-fwk-design.pdf
|
|
|
|
Mar 4
|
Midterm Exam
|
|
|
|
|
Mar 8
|
|
|
|
|
10:30am: Assignment 7: Framework
Specification |
Mar 9,
11
|
No Class -- Spring Break
|
Mar 16
|
Testing, Midterm Discussion,
Plural for Frameworks
|
16-testing.pdf;
16-mini-eclipse-plural.pdf
|
|
|
|
| Static Analysis and Model Checking |
Mar 18
|
Introduction to Static Analysis
|
17-intro-static-analysis.pdf
|
Lect17.doc
|
Checking System
Rules Using System-Specific, Programmer-Written Compiler Extensions |
|
Mar 23
|
Dataflow Analysis Frameworks
|
18-dataflow-analysis.pdf
|
Lect18.pdf
|
dataflow-notation.pdf; dataflow-notation.tex; Nielson
text (optional) |
Assignment 8: Framework/Plugin
Implementation (Part I)
|
Mar 25
|
Dataflow Analysis Examples and
Correctness
|
19-dataflow-examples-correctness.pdf
|
Lect19.doc
|
A
Static Analyzer for Finding Dynamic Programming Errors;
Assuring
and Evolving Concurrent Programs: Annotations and Policy |
|
Mar 30
|
Framework / Plugin
Implementation Presentations |
checkers1-09.pdf
checkers2-09.pdf
connect4-09.pdf
hnefatafl-09.pdf
|
|
|
Assignment 9: Framework/Plugin
Implementation (Part II) |
Apr 1
|
Model Checking |
21-model-checking.pdf
|
|
Clarke et al., Model
Checking, ch. 1-4 |
|
| Analysis Across the Software Lifecycle |
Apr 6
|
Asymptotic Performance
Analysis, Profiling, Real-Time Scheduling
|
22-performance-realtime.pdf
|
Lect22.doc
|
|
|
Apr 8
|
Tool Experience Presentations |
2009
tool presentations
|
|
|
Assignment 10: Tool Project;
Tool list; Powerpoint
template |
| Apr 13 |
Tool Experience Presentations |
|
|
|
|
Apr 15
|
Statistical Analysis of
Reliability
|
25-ReadingTeaLeaves..pdf
|
|
|
Assignment 11: Static
Analysis
|
| Apr 20 |
Security I
|
26-security.pdf
|
Lect26.doc
|
Why
Cryptosystems Fail
|
|
| Apr 22 |
Security II
|
(same)
|
Lect27.doc
|
|
Assignment 12: QA Plan |
Course Wrap-up
|
| Apr 27 |
Web Security (Ph.D. project)
|
28-web-security.pdf
|
|
|
|
Apr 29
|
Case Study: Analysis at Microsoft
|
29-quality-at-microsoft.pdf;
29-static-anal-at-microsoft.pdf
|
|
|
Assignment 13: Security Analysis
|
May 4
|
9:30am - Final Exam
|
|
|
|
|
Academic
partner of Esterel Technologies,
the provider of model-based solutions for DO-178B and IEC 61508
safety-critical
systems.
