Workshop on Advances in Verification for Eiffel (WAVE) 2012
                 Co-located with TOOLS EUROPE 2012
                29 May 2012, Prague, Czech Republic

                     http://wave.inf.ethz.ch


                         Call for Papers

Correctness of software systems can be demonstrated by using static
verification techniques such as theorem provers, model checkers and
exhaustive testing. Static verifiers such as Spec# and ESC/Java have
been developed for object-oriented languages.  These verifiers have
been shown to be feasible to apply to languages such as C# and Java,
though the usability of the tools is still under investigation.

The Eiffel language introduces significant challenges and
opportunities for verification, both of correctness and for property
checking. Eiffel's support for Design by Contract enables scalable and
practical verification, while its expressive object-oriented model
raises verification challenges that push state-of-the-art verification
technology to the limit.

This workshop focuses on advancing the state-of-the-art in
verification technology for Eiffel. It will present work in progress
as well as mature research and development results that address
particular problems in verifying Eiffel software systems, both in
terms of correctness and in terms of property checking (e.g., liveness
or deadlock freedom for SCOOP programs). Research that demonstrates
how verification techniques and tools for other languages (e.g., Java,
C#, Ruby, Python) can be adapted or directly applied to Eiffel
programs are particularly welcome, as are case studies or experiments
in verification.

Specific topics of interest at the workshop include, but are not
limited to:

- Theorem proving techniques applied to Eiffel programs
- Denotational, operational and algebraic theories for contracts
- Model checking applied to Eiffel programs
- Automated testing techniques applied to Eiffel programs
- Tools for verification of Eiffel programs
- Verification techniques for other languages adapted to Eiffel
   programs
- Verification techniques for other languages applied directly to
   Eiffel programs
- Novel case studies or experiments in Eiffel verification
- Proof-carrying code as applied to Eiffel
- Techniques and tools for checking properties of Eiffel programs.

Prospective authors are welcome to contact the workshop organisers to
help clarify whether their work would be relevant to the workshop.


Submissions

The workshop solicits three types of papers:

- Work-in-progress papers, demonstrating novel, promising or unusual
research related to the topics above. These papers should be around
5-7 pages in LNCS format and should clear describe what is novel or
promising about the work.

- Research or experimental papers, demonstrating novel research
results that are reasonably mature, and that would benefit from
feedback and discussion at the workshop. These papers should be around
10-15 pages in LNCS format.

- Tool papers, which describe novel tools for supporting
verification. These papers should clearly describe what is novel about
the tool, and should be around 5-7 pages in LNCS format.

All papers will be peer-reviewed by the organisers and the programme
committee, focusing on suitability for the workshop, novelty, and
whether the work would lead to interesting discussions. Additional
feedback will be provided during the workshop.


Publication & Submission

Accepted papers will appear in the workshop proceedings published as a
CEUR workshop volume with an ISBN. A special issue of the Journal of
Object Technology for extended versions of papers is under
negotiation.

Submission can be made through EasyChair.


Dates

Submission: 24 April 2012
Notification: 8 May 2012
Camera ready copy: 15 May 2012
Workshop date: 29 May 2012


Workshop Organisers

Richard Paige, University of York, UK
Bertrand Meyer, ETH Zurich, Switzerland
Scott West, ETH Zurich, Switzerland


Program Committee

To be announced