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:
Prospective authors are welcome to contact the workshop organisers to help clarify whether their work would be relevant to the workshop.
The workshop solicits three types of papers:
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.
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 .
Submission: 2 May 2012 (extended from 24 April 2012)
Notification: 8 May 2012
Camera ready copy: 15 May 2012
Workshop date: 29 May 2012
Richard Paige, University of York, UK
Bertrand Meyer, ETH Zurich, Switzerland
Scott West, ETH Zurich, Switzerland