International Workshop on Software Verification and Validation (SVV 2004)

In Conjunction with
International Conf. on Formal Engg. Methods (ICFEM) 2004

Seattle (USA), November 8 2004

• Technical Programme
• Goal of the Workshop
• Topics Covered
• Submissions Information
• Program Committee
• Invited Speakers
• Organizers
• Past SVV Workshops

Goal of the Workshop

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.

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

Submissions Information

• Regular submissions should be no more than 15 pages. Short papers (upto 5 pages) describing initial ideas are also welcome. All submitted papers should be in PS or PDF. Please avoid using zip, gzip, compress, tar etc. Papers should be submitted via e-mail to supratik@saul.cis.upenn.edu

• The deadlines are as follows.

  • Submission deadline:  October 8, 2004
  • Notification of Acceptance:  October 22, 2004
  • Final Version submission:  November 1, 2004

 Program Committee

• Tevfik Bultan (University of California, Santa Barbara)

• Michael Co'lon (Naval Research Laboratory, USA)

• Giorgio Delzanno (University of Genova, Italy)

• Sandro Etalle (University of Twente, Netherlands)

• John Goodenough (Software Engineering Institute, CMU, USA)

• Sandeep Kumar Shukla (Virginia Tech USA)
   

Invited Speakers

• Shaz Qadeer, Microsoft Research, USA.
  Title: Context-bounded model checking of concurrent software
  Abstract: Designing concurrent programs is difficult. The nondeterministic interaction between concurrently executing threads of a concurrent program results in programming errors that are notoriously difficult to reproduce and fix. Automated program analysis techniques for finding such errors are invaluable as a debugging and programming aid. In this talk, I will present a novel static analysis technique for concurrent software based on the idea of context-bounded model checking. An execution of a concurrent program is a sequence of contexts, where each context is an uninterrupted sequence of transitions performed by a single thread. Our work is motivated by our observation that many subtle errors in a concurrent program are manifested by executions with few contexts. I will first present KISS (Keep It Simple and Sequential), a technique for transforming a concurrent program P into a sequential program Q that encodes all executions of P with a small number of contexts. We used KISS to convert SDV (Static Driver Verifier), a model checker for sequential C programs, into a model checker for concurrent C programs. The combination of KISS and SDV has found a variety of subtle concurrency errors in Windows device drivers. Next, I will present a new theoretical result which shows that bounding the number of contexts significantly reduces the complexity of verifying concurrent programs. It is well-known that the problem of verifying assertions in a concurrent boolean program is undecidable. I will show that if analysis is limited to executions with a fixed but arbitrary context-bound, the problem becomes decidable, even in the presence of unbounded dynamic thread creation.

• Margus Veanes, Microsoft Research, USA
  Title: A Game approach to Software Testing
  Abstract : We give a brief overview of the model-based testing tool SpecExplorer developed at Microsoft Research and the modeling language Spec# used by SpecExplorer. The tool supports nondeterminism and provides a view of testing a nondeterministic system as a two player game. Generated tests are considered as game strategies. The underlying conformance relation is given by alternating refinement of interface automata.

Organizers

• Ramesh Bharadwaj, Naval Research Laboratory, USA.
• Supratik Mukhopadhyay, West Virginia University, USA. (Workshop Co-ordinator).
• Abhik Roychoudhury, National University of Singapore, Singapore.

If you have any queries about the workshop, please send e-mail to supratik@saul.cis.upenn.edu

Past  SVV Workshops

• SVV 2003, December 14, 2003, Venue: Mumbai (India).