Academic
partner of Esterel EDA Technologies provider
of ESL synthesis for control-intensive IP design and
verification, including SystemC, VHDL, and Verilog code generation
| Date |
Topic |
Slides |
Participation |
Reading |
Assignment
Due |
| Introduction |
|||||
| Jan 15 |
Overview
of Analysis Techniques |
1-course-intro.pdf |
Lect01.doc |
||
| Traditional Analysis: Testing and Inspection | |||||
| Jan 17 | Testing: Techniques |
2-testing.pdf |
Lect02.doc | What is software testing? And why is it so hard?; Kaner text (optional) | |
| Jan 22 | Testing: Processes | (same) |
Lect03.doc | Assignment 1: Testing |
|
| Jan 24 | Testing: Tools |
4-testing.pdf |
Lect04.doc | ||
| Jan 29 |
Inspection | 5-inspection.pdf |
Lect05.doc |
(optional) Wiegers text | Assignment 2: Testing |
| Program Semantics and Verification |
|||||
| Jan 31 | Testing wrap-up |
(same) |
Lect06.doc |
||
| Feb 5 |
Program Semantics and Proofs | 7-semantics.pdf | Lect07.doc |
Notes: 7-semantics.pdf (source 7-semantics.tex) | Assignment 3: Inspection |
| Feb 7 |
Semantics, continued |
Lect08.doc |
|||
| Feb 12 | Hoare Logic: Reasoning about Correctness | 9-hoare.pdf |
Lect09.doc | 3-hoare-notes.pdf; 3-hoare.tex; An Axiomatic Basis for Computer Programming | |
| Feb 14 | ESC/Java: Code Verification | 10-escjava.pdf |
Lect10.doc |
Multiply.java; Multiply-full.java; SimpleSet.java; SimpleSet-full.java | Assignment 4: Semantics and Hoare Logic |
| Static Analysis | |||||
| Feb 19 | Introduction to Dataflow
Analysis |
11-dataflow.pdf |
Lect11.doc |
Checking System Rules Using System-Specific, Programmer-Written Compiler Extensions | Assignment 5: Checking Code with ESC/Java; Stack.java; StackCheck.java |
| Feb 21 | Data Flow Analysis Frameworks |
12-crystal-and-examples.pdf |
dataflow-notation.pdf; dataflow-notation.tex | ||
| Feb 26 | Program Representation and Bug
Finders; Soundness |
13-bug-finder-analysis-soundness.pdf |
Lect13.pdf |
|
|
| Feb 28 |
Interprocedural Analysis: PREfix |
14-prefix.pdf;
14-interprocedural.pdf |
A Static Analyzer for Finding Dynamic Programming Errors | Assignment 6: Simple Data Flow Analysis | |
| Mar 4 |
Static Analysis in Practice |
15-analysis-at-microsoft.pdf;
15-analysis-wrapup.pdf |
Assignment 7: Interprocedural Data Flow Analysis | ||
| Mar 6 |
Midterm |
||||
| Mar 7 |
Tool
Project Bids |
||||
| Mar 11,
13 |
No Class -- Spring Break |
||||
| Design Analysis |
|||||
| Mar 18 |
Security: Background and Motivation | 16-security.pdf |
Lect16.doc |
Why Cryptosystems Fail | |
| Mar 20 |
Security Analysis: STRIDE | (same) |
Lect17.doc | Tool
Interim Report |
|
| Analysis Tools in the Real World |
|||||
| Mar 25 |
Tool Experience Presentations | 2006: tools-day-1.pdf | Assignment
8: Tool Project; Tool list; Powerpoint template |
||
| Mar 27 |
Tool Experience Presentations | 2006: tools-day-2.pdf | |||
| Analysis Across the Software Lifecycle | |||||
| Apr 1 |
Performance Analysis: Profiling,
Monitoring, Scalability |
17-performance.pdf |
|||
| Apr 3 |
Guest Lecture: Klocwork Static
Analysis |
(proprietary; not available) |
Assignment 9: Security Analysis | ||
| Apr 8 |
Design Patterns |
19-patterns.pdf;
see example patterns slides on Blackboard |
|||
| Apr 10 | Design Patterns | Assignment 10: Profiling | |||
| Apr 15 |
Concurrency Analysis | 21-concurrency.pdf |
Assuring and Evolving Concurrent Programs: Annotations and Policy | ||
| Apr 17 |
No class -- Spring
Carnival |
Assignment 11: Design Patterns | |||
| Apr 22 | No
class |
||||
| Apr 24 | Protocol Checking |
protocol-checking.pdf |
The
Fugue Protocol Checker: Is Your Software Baroque? |
||
| Apr 29 |
Ph.D. presentations,
supplementary topics |
Clarke et al., Model Checking, ch. 1-4 | Assignment 12: QA Plan |
||
| May 1* |
Final Exam |
||||
| May 5 |
5:30pm - QA review documents due |
||||
| May 8 |
5:30-8:30PM: QA Plan
Presentations |
Revised QA Plan, QA plan presentations |
|||
Academic
partner of Esterel EDA Technologies provider
of ESL synthesis for control-intensive IP design and
verification, including SystemC, VHDL, and Verilog code generation
Academic
partner of Esterel Technologies,
the provider of model-based solutions for DO-178B and IEC 61508
safety-critical
systems.
| Real-Time |
|||||
| Analysis of Models | Alloy home page | ||||
| Scalability |
|
||||
| Dynamic Analysis | Dynamically Discovering Likely Program Invariants to Support Program Evolution | ||||
| Design Analysis | Assignment 10: Design Analysis: DSMs and Alloy | ||||
| Model Driven Development | |||||
| Model Checking Code |
|||||
| Language and Type Systems |