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

SAVCBS 2008 Workshop Talks

Invited Talk

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

Papers

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 [PPT]
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 [PPT]
George Karabotsos, Concordia University, Canada
Patrice Chalin, Concordia University, Canada
Perry R. James, Concordia University, Canada
Leveda Giannas, Concordia University, Canada

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

Using Analysis Patterns to Uncover Specification Errors [PPT]
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

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 [PPT]
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

Challenge Problem Solutions

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

[PPT]
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

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