Workshop on Verified Software: Theory, Tools, and Experiments
VSTTE 2009

Monday November 2, 2009
Eindhoven, the Netherlands
Affiliated with Formal Methods Week.

Important Dates


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:

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.


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


Participants can already register for VSTTE and make hotel reservations for their stay in Eindhoven using the FMweek registration page.


VSTTE proceedings will be published as a special issue of the Software Tools for Technology Transfer (STTT) journal.

Program Committee

Previous VSTTEs