SAVCBS'04
	Specification and Verification of Component-Based Systems
	Workshop at ACM SIGSOFT 2004/FSE-12 October 31-November 1, 2004

Cover Page, Table of Contents, and Introduction

Sunday, October 31, 2004

Paper Session 1

Verification of Multithreaded Object-oriented Programs with Invariants
Bart Jacobs, Katholieke Universiteit Leuven
K. Rustan M. Leino, Microsoft Research
Wolfram Schulte, Microsoft Research

Paper Session 2

Encapsulating Concurrency as an Approach to Unification
Santosh Kumar, The Ohio State University
Bruce W. Weide, The Ohio State University
Paolo A. G. Sivilotti, The Ohio State University
Nigamanth Sridhar, Cleveland State University
Jason O. Hallstrom, Clemson University
Scott M. Pike, Texas A&M University

Basic Laws of Object Modeling
Rohit Gheyi, Federal University of Pernambuco
Tiago Massoni, Federal University of Pernambuco
Paulo Borba, Federal University of Pernambuco

Selective Open Recursion: Modular Reasoning about Components and Inheritance
Jonathan Aldrich, Carnegie Mellon University
Kevin Donnelly, Boston University

Poster Session

UML Automatic Verification Tool (TABU)
M. Encarnación Beato, Universidad Pontificia de Salamanca
Manuel Barrio-Solórzano, Universidad de Valladolid
Carlos E. Cuesta, Universidad de Valladolid

Integration of Legacy Systems in Software Architecture
Maria Wahid Chowhury, University of Victoria
Muhammad Zafar Iqbal, Shah Jalal University of Science and Technology

Toward Specification and Composition of BoxScript Components
H. Conrad Cunningham, University of Mississippi
Yi Liu, University of Mississippi
Pallavi Tadepalli, University of Mississippi

Hierarchical Presynthesized Components for Automatic Addition of Fault-Tolerance: A Case Study
Ali Ebnenasir, Michigan State University
Sandeep Kulkarni, Michigan State University

Using Wrappers to add Run-Time Verification Capability to Java Beans
Vladimir Glina, Virginia Tech
Stephen Edwards, Virginia Tech

Integrating Specification and Documentation in an Object-Oriented Language
Jie Liang, McMaster University
Emil Sekerinski, McMaster University

Designing a Programming Language to Provide Automated Self-Testing for Formally Specified Software Components
Roy Patrick Tan, Virginia Tech
Stephen H. Edwards, Virginia Tech

Open Incremental Model Checking (Extended Abstract)
Nguyen Truong Thang, Japan Advanced Institute of Science and Technology
Takuya Katayama, Japan Advanced Institute of Science and Technology

Toward Structural and Behavioral Analysis For Component Models
Hanh-Missi Tran, Université des Sciences et Technologies de Lille
Philippe Bedu, Electricité de France
Laurence Duchien, Université des Sciences et Technologies de Lille
Hai-Quan Nguyen, Electricité de France
Jean Perrin, Electricité de France

Paper Session 3

CTL Model-checking for Systems with Unspecified Finite-State Components
Gaoyan Xie, Washington State University
Zhe Dang, Washington State University

Automatic Extraction of Sliced Object State Machines for Component Interfaces
Tao Xie, University of Washington
David Notkin, University of Washington

Demonstrations 1

The RESOLVE Compiler
Greg Kulczycki, Virgina Tech
John Hunt, Clemson University
Murali Sitaraman, Clemson University

Monday, November 1, 2004

Paper Session 4

Formalizing Lightweight Component Composition Verification
Stephen McCamant, Massachusetts Institute of Technology
Michael D. Ernst, Massachusetts Institute of Technology

Verification of Evolving Software
Sagar Chaki, Carnegie Mellon University
Natasha Sharygina, Carnegie Mellon University
Nishant Sinha, Carnegie Mellon University

Paper Session 5

Compositional Quality of Service Semantics
Richard Staehli, Simula Research Laboratory
Frank Eliassen, Simula Research Laboratory

An Analysis Framework for Security in Web Applications
Gary Wassermann, University of California, Davis
Zhendong Su, University of California, Davis

Paper Session 6

Synthesis of "Correct" Adaptors for Protocol Enhancement in Component-based Systems
Marco Autili, University of L'Aquila
Paola Inverardi, University of L'Aquila
Massimo Tivoli, University of L'Aquila
DavidGarlan, Carnegie Mellon University

Monitoring Design Pattern Contracts
Jason O. Hallstrom, Clemson University
Neelam Soundarajan, The Ohio State University
Benjamin Tyler, The Ohio State University

DEET for Component-Based Software
Murali Sitaraman, Clemson University
Durga P. Gandi, Clemson University
Wolfgang Küchlin, Universität Tübigen
Carsten Sinz, Universität Tübigen
Bruce W. Weide, The Ohio State University

Demonstrations 2

Petshop: A Tool for the Behavioral Specification of Distributed Component-Based Systems
Rémi Bastide, Université Toulouse 1

Spec#: A .NET Language for Software Contracts

Mike Barnett, Microsoft Research
Rob DeLine, Microsoft Research
Manuel Fahndrich, Microsoft Research
K. Rustan M. Leino, Microsoft Research
Wolfram Schulte, Microsoft Research
Herman Venter, Microsoft Research