Workshop affiliated with CAV 2006

Workshop on Verification and Debugging (V&D'06)

Note: this is a preliminary web site. We will complete a CFP ASAP.

CAV 2006 is part of FLOC, in Seattle.

Motivation

Knowing that a design does not fulfill its specification is only a first step towards a correct system. The violation may be caused by a fault in the design, the specification, or the constraints on the environment. The designer needs to understand the failure and to locate and correct the fault.

Industrial experience shows that fault localization and correction take much more time, effort, and expense than fault detection. Also, debugging often takes place right before the release of the design, which makes it a high-risk, high-stakes activity that may, if not done quickly and correctly, delay the release of a product. Automated help at debugging can thus be very valuable.

Yet, localization and correction have received relatively little attention in the CAV community and the work done on this subject is spread between the computer aided verification, software engineering, and model-based diagnosis communities. The Workshop on Verification and Debugging aims to bring these communities together to stimulate exchange of information and common research on the subject.

Significance

The workshop is of primary significance to the researchers in computer-aided verification, in model-based diagnosis, and software engineering, particularly in dynamic program analysis and debugging. It is also of relevance to people in automated reasoning, logics, satisfiability testing, and automated deduction given the importance of those techniques for debugging.

Fault detection has seen enormous improvements in the past – due in particular to the efforts of the CAV community. When it comes to localizing and correcting these faults, researchers in the verification and software engineering communities have also made important progress, but in (thus far) separated camps. In particular, we expect the workshop to animate the exchange of ideas and to stimulate cross-fertilization, in order to put together the best of two worlds.

Goals and Topics

The workshop intends to attract work in the areas of algorithms, tools, and methodologies for failure analysis. This includes work on

• explaining counter-examples,
• simplifying counter-examples,
• fault localization,
• repairing the model, the specification, or the environment description,
• test case generation, and
• empirical studies on the types of faults that occur.

Program Committee

• Roderick Bloem (Graz University of Technology),
• Alex Groce (NASA Jet Propulsion Lab),
• John Moondanos (Future Formal Technologies Group, Logic Design Group, Intel),
• Marco Roveri (ITC-irst),
• Fabio Somenzi (University of Colorado),
• Markus Stumptner (Univeristy of Southern Australia), and
• Andreas Zeller (University of Saarbruecken).

info: roderick.bloem@ist.tugraz.at