International Workshop on
Software Verification and Validation (SVV 2004)
In Conjunction with
Conf. on Formal Engg. Methods (ICFEM) 2004
Seattle (USA), November 8
Details about the Workshop
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
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
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
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
- Tools, environments and case studies for large scale software verification
- Static analysis/Abstract interpretation/Program transformations for
- 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
- Integrating testing and run-time monitoring with formal techniques
- Validation of UML diagrams, and/or requirement
- Software certification and proof carrying code
- Integration of formal verification into software development projects
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 email@example.com
The deadlines are as follows.
- Submission deadline: October 8, 2004
- Notification of Acceptance: October 22, 2004
- Final Version submission: November 1, 2004
Tevfik Bultan (University of
California, Santa Barbara)
Michael Co'lon (Naval Research
Giorgio Delzanno (University of
Sandro Etalle (University of Twente,
John Goodenough (Software
Engineering Institute, CMU, USA)
Sandeep Kumar Shukla (Virginia Tech
- Shaz Qadeer, Microsoft Research, USA.
Title: Context-bounded model checking of concurrent software
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
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.
Ramesh Bharadwaj, Naval Research Laboratory, USA.
Supratik Mukhopadhyay, West Virginia University, USA. (Workshop
Abhik Roychoudhury, National
University of Singapore, Singapore.
If you have any queries about the workshop, please send e-mail to
Past SVV Workshops
- SVV 2003, December 14, 2003,
Venue: Mumbai (India).