Scope: VSTTE 2008 invites submissions of technical papers on all aspects of verified software covering theoretical as well as experimental. The topics include requirements modeling, specification languages, specification case-studies, formal calculi, programming languages, language semantics, software design methods, software testing, automatic code generation, refinement methodologies, type systems, computer security, verification tools (static analysis, dynamic analysis, model checking, theorem proving, satisfiability), benchmarks, challenge problems, and integrated verification environments. We are especially interested in specific challenges such as

• POPLMark: http://alliance.seas.upenn.edu/~plclub/cgi-bin/poplmark/
• File system: http://www.cs.york.ac.uk/circus/mc/abz
• Medical devices: http://www.cas.mcmaster.ca/sqrl/pacemaker.htm

Invited Talks:

• Andreas Podelski, University of Freiburg.
  Verification, Least-Fixpoint Checking, Abstraction
• Sriram Rajamani, Microsoft Research.
  Combining Tests and Proofs
• John Reynolds, Carnegie-Mellon University.
  Readable Formal Proofs
• Moshe Vardi, Rice University.
  From Verification to Synthesis

• Eric Hehner.
  Practical Predicative Programming Primer
• Ernie Cohen.
  Verifying the Microsoft Hypervisor
• Leonardo de Moura.
  SMT@Microsoft

• Artem Starostin and Alexandra Tsyban.
  Verified Process-Context Switch for C-Programmed Kernels
• Yoshifumi Yuasa, Yoshinori Tanabe, Toshifusa Sekizawa and Koichi Takahashi.
  Verification of the Deutsch-Schorr-Waite marking algorithm with Modal Logic
• Xinyu Feng, Zhong Shao, Yu Guo and Yuan Dong.
  Combining Domain-Specific and Foundational Logics to Verify Complete Software Systems
• Bruce Weide, Murali Sitaraman, Heather K. Harton, Bruce Adcock, Paolo Bucci, Derek Bronish, Wayne D. Heym, Jason Kirschenbaum and David Frazier.
  Incremental Benchmarks for Software Verification Tools and Techniques
• Dhammika Elkaduwe, Gerwin Klein and Kevin Elphinstone.
  Verified Protection Model of the seL4 Microkernel
• Gerwin Klein and Rafal Kolanski.
  Mapped Separation Logic
• Eyad Alkassar, Mark Hillebrand, Dirk Leinenbach, Norbert W. Schirmer and Artem Starostin.
  The Verisoft Approach to Systems Verification
• Eyad Alkassar and Mark Hillebrand.
  Formal Functional Verification of Device Drivers
• Mark Bickford.
  Unguessable Atoms: A Logical Foundation for Security
• Joey Coleman.
  Expression Decomposition in a Rely/Guarantee Context
• Matthias Daum, Jan Dörrenbächer, Burkhart Wolff and Mareike Schmidt.
  A Verification Approach for System-level Concurrent Programs
• Anindya Banerjee, Michael Barnett and David Naumann.
  Boogie Meets Regions: a Verification Experience Report
• Rustan Leino, Peter Müller and Angela Wallenburg.
  Flexible Immutability with Frozen Objects
• Patrice Chalin, Perry R. James and George Karabotsos.
  JML4: Towards an Industrial Grade IVE for Java and Next Generation Research Platform for JML
• Gregory Dennis, Kuat Yessenov and Daniel Jackson.
  Bounded Verification of Voting Software
• Daniel Leivant.
  Propositional dynamic logic for recursive procedures