cs296-1, Spring 2003

Time: Wednesday, 1500-1730 hrs
Location: CIT 219

Course Professor: Shriram Krishnamurthi

We will study topics from programming languages and computer-aided verification, with particular emphasis on their intersection.  I will run the course in seminar format, expecting students to complete readings, presentations and, possibly, also programming or tool evaluation projects. If you have questions, please contact me.

Course Schedule

Jan
 Feb
 Mar
 Apr
29
 5
 12
 19
 26
 5
 12
 19
 2
 9
 16
 23
 30
   
Types for Atomicity (Tucker/Wicks, Jan 29) - scribe notes (internal access only)
Flanagan, Qadeer
 Types for Atomicity (PS)
Types for Atomic Interfaces (email from Dave Tucker)

Implicit Invocation Systems (Cooper/Tucker, Feb 5) - scribe notes (internal access only)
Shaw, Garlan, et al
 Reasoning about Implicit Invocation (PDF)
Lessons on Converting Batch Systems to Support Interaction (Web page)
Architectural Mismatch, or Why it's hard to build a system out of existing parts (PDF)

Verifying Interactive Services (Licata/Blundell, Feb 12) - scribe notes (internal access only)
Godefroid, et al
 VeriWeb: Automatically Testing Dynamic Web Sites (PS)
De Alfaro
 Model Checking the World Wide Web (PS, PDF)
Godefroid, et al
 Automated Systematic Testing for Constraint-Based Interactive Services (PS)

Survey of Security (Triandopoulos/Wooldridge, Feb 19) - scribe notes (internal access only)
Sabelfeld, Myers
 Language-Based Information Flow Security (PS, PDF)
Schneider, Morrisett, Harper
 A Language-Based Approach to Security (PS)

Using Multi-Valued and Modal Logics (Chechik/no scribe, Feb 26)
Chechik is visiting Brown; she will speak about her work to the class
Easterbrook, Chechik, et al
 Multi-Valued Symbolic Model-Checking (PS)
A Framework for Multi-Valued Reasoning over Inconsistent Viewpoints (PS)
Godefroid, et al
 Generalized Model Checking: Reasoning about Partial State Spaces (PS)
Abstraction-based Model Checking using Modal Transition Systems (PS)

Analyzing Software Architectures (Wooldridge/Montgomery, Mar 5) - scribe notes (internal access only)
Naumovic, Avrunin, Clarke, Osterweil
 Applying Static Analysis to Software Architectures (PS)
Magee, Kramer, Giannakopoulou, et al
 Behavior Analysis of Software Architectures (PDF)
Garlan, et al
 Specifying and Analyzing Dynamic Software Architectures (paper)

Model Exploration with Queries (Blundell/Licata, Mar 12) - scribe notes (internal access only)
Chan
 Temporal-Logic Queries (CAV 2000)
Chechik, et al
 Model Exploration with Temporal Logic Query Checking (PS)

Model Generation (Goldwater/Cooper, Mar 19) - scribe notes (internal access only)
Jackson, et al
 Automating First-Order Relational Logic (PDF)
A Micromodularity Mechanism (PDF)

Programming With Software Architectures (Eddon/Weston, Apr 2) - scribe notes (internal access only)
Aldrich, Chambers, Notkin
 ArchJava: Connecting Software Architecture to Implementation (PDF)
Architectural Reasoning in Java (PDF)

Interface Automata (Weston/Goldwater, April 9) - scribe notes (internal access only)
De Alfaro, Henzinger
 Interface Automata (PS, PDF)
Synchronous and Bidirectional Component Interfaces (PS, PDF) — read this paper for the excellent introductory material alone

FLAVERS and Bandera (Montgomery/Marceau, April 16) - scribe notes (internal access only)
In addition, Dwyer will speak at Brown on April 22
Cobleigh, Clarke, Osterweil
 FLAVERS (PS)
Dwyer, Hatcliff, Păsăreanu, et al
 Tool-Supported Program Abstraction for Finite-State Verification (PDF)
Filter-Based Model Checking of Partial Systems (PDF)

The SLAM Project (Marceau/Eddon, April 23) - scribe notes (internal access only)
Ball, et al
 Boolean and Cartesian Abstractions for Model Checking C Programs (TACAS 2001)
Automatically Validating Temporal Safety Properties of Interfaces (PS,PDF)
Automatic Predicate Abstraction of C Programs (PS,PDF)

Erlang Verification (Wicks/no scribe, April 30)
Dam, et al
 Toward Parametric Verification of Open Distributed Systems (paper)