Specification and Verification of Component-Based Systems

- Workshop at OOPSLA 2001 -

October 14, 2001
Marriott Hotel, Meeting Room 1


8:30AM: Welcome
    Gary T. Leavens, Iowa State University

8:35AM: Session I: Specification-Based Testing and Run-Time Analysis
    Chair: Markus Lumpe, Iowa State University

Testing Components
Neelam Soundarajan, The Ohio State University
Benjamin Tyler, The Ohio State University

Spying on Components: A Runtime Verification Technique
Mike Barnett, Microsoft Research
Wolfram Schulte, Microsoft Research

Toward Reflective Metadata Wrappers for Formally Specified Software Components
Stephen H. Edwards, Virginia Tech.

10:05AM: Break

10:20AM: Discussion of Session I Topics

10:50AM: Session II: Architecture and Composition
    Chair: Dimitra Giannakopoulou, NASA Ames Research Center

Architectural Reasoning in ArchJava
Jonathan Aldrich, University of Washington
Craig Chambers, University of Washington

Using Message Sequence Charts for Component-based Formal Verification
Bernd Finkbeiner, Stanford University
Ingolf Krüger, Technical University of Munich

11:50AM: Discussion of Session II Topics

12:10PM: Lunch (on your own)

1:15PM: Session III: Keynote by Clemens Szyperski, Microsoft Research
    Chair: Murali Sitaraman, Clemson University

2:00PM: Session IV: Compositional Verification
    Chair: Gary T. Leavens, Iowa State University

Reasoning about Composition: A Predicate Transformer Approach
Michel Charpentier, University of New Hampshire

Specification and Verification with References
Bruce W. Weide, The Ohio State University
Wayne Heym, The Ohio State University

3:00PM: Break

3:15PM: Session IV: Compositional Verification Continued

Modular Verification of Performance Correctness
Joan Krone, Denison University
William F. Ogden, The Ohio State University
Murali Sitaraman, Clemson University
3:45PM: Discussion of Session IV Topics

4:15PM - 5:30PM: General Discussion