SAVCBS'08
	Specification and Verification of Component-Based Systems
	Workshop at SIGSOFT 2008/FSE 16 November 9-10, 2008

SAVCBS 2008 Workshop Program

Georgia Tech Hotel and Conference Center, room "Conference A"

Cover Page, Table of Contents, and Introduction

Sunday, November 9, 2008

8:45 Welcome and Introduction

9:00-10:15 Invited Talk

Verification Challenges for Components in Federated Distributed Systems
Wolfgang Emmerich, London Software Systems and University College London, UK

10:15-11:00 Break

11:00-12:30 Challenge Problem Solutions I

Formalizing Design Patterns: A Comprehensive Contract for Composite
Jason Hallstrom, Ohio State University, USA
Neelam Soundarajan, Ohio State University, USA

Verifying the Composite Pattern using Separation Logic
Bart Jacobs, Katholieke Universiteit Leuven, Belgium
Jan Smans, Katholieke Universiteit Leuven, Belgium
Frank Piessens, Katholieke Universiteit Leuven, Belgium

Permissions to Specify the Composite Design Pattern
Kevin Bierhoff, Carnegie Mellon University, USA
Jonathan Aldrich, Carnegie Mellon University, USA

12:30-2:00 Lunch

2:00-2:30 Challenge Problem Solutions II

Model Programs for Preserving Composite Invariants
Steve Shaner, Iowa State University, USA
Hridesh Rajan, Iowa State University, USA
Gary T. Leavens, University of Central Florida, USA

2:30-3:00 Challenge Problem Discussion

3:00-3:30 Break

3:30-4:30 Short Papers

Component-Based Design in Tako: A Case Study
Arun Sudhir, Virginia Tech, USA
Gregory Kulczycki, Virginia Tech, USA
Jyotindra Vasudeo, Hillcrest Laboratories, USA

Integrating Math Units and Proof Checking for Specification and Verification
Hampton Smith, Clemson University, USA
Kim Roche, Clemson University, USA
Murali Sitaraman, Clemson University, USA
Joan Krone, Denison University, USA
William F. Ogden, Ohio State University, USA

Using Isabelle Theories to Help Verify Code That Uses Abstract Data Types
Jason Kirschenbaum, Ohio State University, USA
Bruce Adcock, Ohio State University, USA
Derek Bronish, Ohio State University, USA
Paolo Bucci, Ohio State University, USA
Bruce Weide, Ohio State University, USA

4:30-5:30 Poster Session

Formal Tolerant Software/Hardware Architecture
Philippe Devienne, LIFL, CNRS, Lille University, France
Rabih OUEIDAT, LIFL, CNRS, Lille University, France

Specifying Reactive Systems
Nigamanth Sridhar, Cleveland State University, USA
Jason Hallstrom, Clemson University, USA

Monday, November 10, 2008

8:30-10:00 Full Papers I

Distributed Multi-threaded Verification of Java Programs
Perry R. James, Concordia University, Canada
Patrice Chalin, Concordia University, Canada
Leveda Giannas, Concordia University, Canada
George Karabotsos, Concordia University, Canada

JML and Aspects: The Benefits of Instrumenting JML Features with AspectJ
Henrique Rebêlo, Computing Systems Department - UPE, Brazil
Sergio Soares, Computing Systems Department - UPE, Brazil
Ricardo Lima, Universidade de Pernambuco, Brazil
Paulo Borba, Informatics Center, Federal University of Pernambuco, Brazil
Márcio Cornélio, Computing Systems Department - UPE, Brazil

Total Correctness of Recursive Functions using JML4 FSPV
George Karabotsos, Concordia University, Canada
Patrice Chalin, Concordia University, Canada
Perry R. James, Concordia University, Canada
Leveda Giannas, Concordia University, Canada

10:00-10:30 Break

10:30-12:00 Full Papers II

Adapting JML to generic types and Java 1.6
David Cok Eastman Kodak Company, USA

Using Analysis Patterns to Uncover Specification Errors [PS] [A4 size PS]
William Heaven, Imperial College London, UK
Alessandra Russo, Imperial College London, UK

Extensions of the theory of observational purity and a practical design for JML
David Cok, Eastman Kodak Company, USA
Gary T. Leavens, University of Central Florida, USA

12:00-12:30 Discussion and Wrap-up

12:30-2:00 Lunch

2:00-3:30 Informal Demonstration Session