Overview

Software is playing an important role in economy, government, and military. Since software is often deployed in safety critical applications, correctness and reliability have become issues of utmost importance. Techniques for verification and validation traditionally fall into three main categories. The first category involves informal methods such as software testing and monitoring. The second involves formal verification, i.e., model checking and theorem proving. The third is abstract interpretation and static program analysis techniques.

The goal of this workshop is to promote discussion on novel combinations of these methodologies, as well as study the individual contribution of each of these methodologies in verifying software. An example of a combined verification methodology is the recent research direction that combines abstraction (of infinite-state programs into finite-state ones) with model checking (of finite-state systems).  There is a growing conviction in the research community that such hybrid methodologies are imperative for the process of  analyzing full-fledged software systems. This workshop will study combination of analysis methodologies for verification of software.  This research is very important and timely since:

• Software is being increasingly used to control embedded systems which are often safety critical (such as automobile parts).
• There is renewed promise in program verification in the recent years due to: (a) progress in generating models from code, and (b) combination of model checking with other analysis techniques such as abstract interpretation.

Program

• SVV program
• SVV accepted papers
• SVV pre-proceedings

Invited Talk

• Monday, August 21st, 09:30‑10:30
  Byron Cook (Microsoft Research)
  Automatic Termination Proofs for Systems-level Code [ppt]

Publication

Topics Covered

The workshop will focus on theoretical techniques, practical methods as well as case studies for verification of  conventional and embedded software systems. In particular, we welcome papers which describe combinations of formal and informal reasoning, as well as formal verification and program analysis techniques. Tool papers and case studies, which report on: advances in verifying large scale programs in standard languages are particularly sought. The list of topics include, but are not restricted to:

• Tools, environments and case studies for large scale software verification
• Static analysis/Abstract interpretation/Program transformations for verification
• Use of model checking and deductive techniques for software verification
• Role of declarative programming languages (such as Prolog) for infinite state software verification.
• Techniques to validate system software (such as compilers) as well as assembly code/Java bytecode
• Proof techniques for verifying specific classes of software (such as object-oriented programs)
• Integrating testing and run-time monitoring with formal techniques
• Validation of UML diagrams, and/or  requirement specifications
• Software certification and proof carrying code
• Integration of formal verification into software development projects

Program Committee

• Rajeev Alur, Univ. of Penn. (USA)

• Tevfik Bultan, Univ. of California Santa Barbara (USA)

• Sagar Chaki, Software Engg Institute CMU (USA)

• Maurizio Gabbrielli, Univ. of Bologna (Italy)

• Aarti Gupta, NEC Labs (USA)

• Gopal Gupta, Univ of Texas Dallas (USA)

• Shengchao Qin, Univ. of Durham (UK)

• C.R. Ramakrishnan, Univ. of Stony Brook (USA)

• R.E. Kurt Stirewalt, Michigan State Univ. (USA)

Organizers

• Abhik Roychoudhury, National University of Singapore, Singapore.
• Zijiang Yang, Western Michigan University, USA.

If you have any queries about the workshop, please send e-mail to either of us.

History

• SVV 2003, Mumbai (India).
• SVV 2004, Seattle (USA)
• SVV 2005, Manchester(UK)