Workshop

Program Chairs


Rajeev Joshi

NASA/JPL Laboratory

for Reliable Software

Rajeev.Joshi@jpl.nasa.gov

Joseph Kiniry

University College Dublin

kiniry@ucd.ie


Program Committee

  1. -Michael Butler

  2. -Patrice Chalin

  3. -Rod Chapman

  4. -Rajeev Joshi

  5. -Joseph Kiniry

  6. -Madan Musuvathi

  7. -José Nuno Oliveira

  8. -Robby

  9. -Jack Wileden

  10. -Dan Zimmerman


Conference
Program Chairs

Jim Woodcock

University of York

jim@cs.york.ac.uk

Natarajan Shankar

SRI International

shankar@csl.sri.com


Important Dates

18 August 2008

    Submission deadline

1 September 2008

    Decisions on papers

15 September 2008

    Final versions due

6—9 October 2008

    VSTTE 2008

9 October 2008,  10:30-

    Experiments Workshop

 

VS-EXPERIMENTS 2008 invites submissions of technical and position papers on all aspects of experiments conducted relating to verified software.


We are especially interested in the reflective results of past challenges and ongoing experiments.  Such projects include include the Mondex Case Study, the Verified File System, medical devices, and work on verifying Free/Open Source Software like the Apache webserver and the KOA e-voting platform.


This workshop is meant to be a working workshop.  Participants are responsible for formulating action plans, based upon current experiences and best-practices, for tackling the challenges inherent in identifying, defining, promoting, executing, sharing, maintaining, and publishing the results of scientific experiments in verified software.  A panel session will facilitate these goals.

Scope

Submissions

Submitted research papers and system descriptions must be original and not submitted for publication elsewhere.  Technical research paper submissions are limited to 15 proceedings pages and must include a cogent and self-contained description of the ideas, methods, results, and comparison to existing work.  Position papers are limited to 6 proceedings pages and should include concrete proposals relating to current and future experiments.

Papers can be submitted via EasyChair.  Submissions that arrive late or are too long will not be considered.  The proceedings of VS-EXPERIMENTS 2008 will be published as a technical report at either/both JPL or UCD.  Some papers may be invited for a follow-up publication in a journal.

The main VSTTE Conference will precede the VS-EXPERIMENTS workshop on 6—9 October 2008.  Concurrent with this workshop are two sister workshops: VS-THEORY and VS-TOOLS.  All workshops will focus on formulating action plans for tackling the challenges for verified software.

Workshops

Schedule

Time - Speaker - Topic

10:30-11:00 - Jerome White

    Towards Verified Distributed Software through Refinement of Formal Archetypes

11:00-11:30 - Michael Butler

    Applying Event-B and Rodin to the Filestore

11:30-12:00 - David Cok

    Observations Regarding Improved Usability of SMT Solvers for Debugging Specifications

12:00-13:00 - Lunch

13:00-13:30 - Leonardo de Moura

    Experiments in Software Verification using SMT Solvers

13:30-14:00 - Jim Woodcock

    Proving Correctness of OS Kernels

14:00-14:15  - Miguel Ferreira

    Verifying Intel Flash File System Core

14:15-14:45 - Break

14:45-15:15 - Rod Chapman

    Formal Methods at Praxis

15:15-15:45 - Sebastian Bogan

    Writing Specifications of the User-mode Operating System SOS

15:45-16:00 - Break

16:00-17:00 - Panel Session