Workshop on Verified Software: Theory, Tools, and Experiments
VSTTE 2009
Monday November 2, 2009
Eindhoven, the Netherlands
Affiliated with Formal
Methods Week.
Important Dates
- Submission deadline: September 11, 2009, 11:59pm Samoa time (UTC-11)
- Notification: October 2, 2009
- Final version: October 16, 2009
- Workshop: November 2, 2009
Overview
FM 2009 is the sixteenth in a series of symposia of the
Formal Methods Europe association, and the second one
that is organized as a world congress. Ten years after
FM'99, the 1st World Congress, the formal methods
communities from all over the world will once again have
an opportunity to meet. FM 2009 will be both an
opportunity to celebrate, and an opportunity to join in
when enthusiastic researchers and practitioners from a
diversity of backgrounds and schools come together to
discuss their ideas and experiences.
The workshop on Verified Software: Theories, Tools, and
Experiments (VSTTE 2009) will take place on November the
2nd. The focus of this workshop will be on tools, as
previous VSTTE conferences in Zurich and Toronto
emphasised theories and experiments. Consisting of
contributed papers and invited talks, the workshop will
focus on the tools behind the development of systematic
methods for specifying, building, and verifying
high-quality software. This includes topics like:
- Program logic
- Specification and verification techniques
- Tool support for specification languages
- Tool for various design methodologies
- Tool integration and plug-ins
- Automation in formal verification
- Tool comparisons and benchmark repositories
- Combination of tools and techniques
(e.g. formal vs. semiformal, software specification
vs. engineering techniques)
- Customizing tools for particular applications
Papers about tool architectures, and their achievements
are most welcome. The contributed papers, which should
report on previously unpublished work, can reflect
current and preliminary work in areas of software
verification. New technical results, overviews of new
developments in software verification projects, short
papers accompanying tool demonstrations, as well as
position papers on how to further advance the goal of
verified software are all welcome.
Program
08:30-09:00 - Registration
09:00-10:00 - Invited Speaker: Rajeev Joshi, NASA JPL US
10:00-10:30 - Break
10:30-11:30 - Session 1: Program specifications
Discovering Specifications for Unknown Procedures with Separation Logic
Chenguang Luo, Florin Craciun, Shengchao Qin, Guanhua He and Wei-Ngan Chin.
On Essential Program Annotations and Completeness of Verifying Compilers
Bernhard Beckert, Thorsten Bormer and Vladimir Klebanov.
11:30-12:30 - Invited Speaker: Jim Woodcock, University of York UK
12:30-13:30 - Lunch
13:30-14:30 - Invited Speaker: Pascal Cuoq, CEA France
14:30-15:30 - Session 2: SAT / SMT solvers
SMT Solvers: New Oracles for the HOL Theorem Prover
Tjark Weber.
An Interval-based SAT Modulo ODE Solver for Model Checking Nonlinear Hybrid Systems
Daisuke Ishii, Kazunori Ueda and Hiroshi Hosobe.
15:30-16:00 - Break
16:00-17:00 - Invited Speaker: John McDermott, Naval Research Lab US
Invited Speaker: Kalou Cabrera Castillos, INRIA Nancy France
17:00-17:30 - Discussion session
Registration
Participants can already register for VSTTE and make hotel
reservations for their stay in Eindhoven using the
FMweek
registration page.
Proceedings
VSTTE proceedings will be published as a special issue of
the Software Tools for
Technology Transfer (STTT) journal.
Program Committee
- David Deharbe, Dimap UFRN, Brazil
- Dino Distefano, Queen Mary University of London, UK
- Jean-Christophe
Filliātre (co-chair), CNRS, France
- Leo Freitas
(co-chair), University of York, UK
- John McDermott, Naval Research Laboratory, USA
- Yannick Moy, AdaCore, France
- Arnaud Venet, Kestrel Technology, USA
Previous VSTTEs