Specification and Verification of
Component-Based Systems
Workshop at
November 10-11, 2006

SAVCBS 2006 Workshop Program

Cover Page, Table of Contents, and Introduction

Friday, November 10

Invited Talk

Variance Analyses from Invariance Analyses
Josh Berdine, Microsoft Research


Performance Analysis Based upon Complete Profiles
Joan Krone, Denison University
Murali Sitaraman, Clemson University
William F. Ogden, Ohio State University

Performance Modelling of a JavaEE Component Application using Layered Queuing Networks: Revised Approach and a Case Study
Alexander Ufimtsev, University College Dublin
Liam Murphy, University College Dublin

Soundness and Completeness Warnings in ESC/Java2
Joseph Kiniry, University College Dublin
Alan E. Morkan, University College Dublin
Barry Denby, University College Dublin

Early Detection of JML Specification Errors using ESC/Java2
Patrice Chalin, Concordia University

Challenge Problem Solutions

VC Generation for Functional Behavior and Non-Interference of Iterators
Bart Jacobs, K.U.Leuven
Frank Piessens, K.U.Leuven
Wolfram Schulte, Microsoft Research

Specifying Java Iterators with JML and Esc/Java2
David R. Cok, Eastman Kodak Company

SAVCBS 2006 Challenge: Specification of Iterators
Bruce W. Weide, The Ohio State University

Iterator Specification with Typestates
Kevin Bierhoff, Carnegie Mellon University

Reasoning About Iterators With Separation Logic
Neelakantan Krishnaswami, Carnegie Mellon University

Saturday, November 10


Experiments in the use of tau-simulations for the components-verification of real-time systems
Francoise Bellegarde, LIFC
Jacques Julliand, LIFC
Hassan Mountassir, LIFC
Emilie Oudot, LIFC

JML-based Verification of Liveness Properties on a Class
Julien Groslambert, LIFC
Jacques Julliand, LIFC
Olga Kouchnarenko, LIFC

Using Resemblance to Support Component Reuse and Evolution
Andrew McVeigh, Imperial College
Jeff Kramer, Imperial College
Jeff Magee, Imperial College

Simplifying Reasoning about Objects with Tako
Gregory Kulczycki, Virginia Tech
Jyotindra Vasudeo, Virginia Tech


Automatic Data Environment Construction for Static Device Drivers Analysis
Hendrik Post, University of Tübingen
Wolfgang Küchlin, University of Tübingen

Jonathan Aldrich, Mike Barnett, Dimitra Giannakopoulou, Gary T. Leavens, and Natasha Sharygina

$Date: 2006/11/06 04:25:42 $