[ecoop-info] VerifyThis Competition 2017: Call for verification challenges

[Rosemary Monahan]

********************************************************************************

VerifyThis Verification Competition 2017

FIRST ANNOUNCEMENT AND CALL FOR PROBLEMS

Competition to be held at ETAPS 2017

http://verifythis.ethz.ch

********************************************************************************

Get involved, even if you cannot participate in the competition: provide a challenge.


IMPORTANT DATES
Submission deadline: January 13, 2017
Competition: April 22-23, 2017

CALL FOR PROBLEMS
To extend the problem pool and tender better to the needs of the participants, we are now soliciting verification problems for the competition (itself introduced below):
- a problem should contain an informal statement of the algorithm to be implemented (optionally with complete or partial pseudocode) and the requirement(s) to be verified
- a problem should be suitable for a 60-90 minute time slot
- submission of reference solutions is strongly encouraged
- problems with an inherent language- or tool-specific bias should be clearly identified as such
- problems that contain several subproblems or other means of difficulty scaling are especiallywelcome
- the organizers reserve the right (but no obligation) to use the problems in the competition, either as submitted or with modifications
- submissions from (potential) competition participants are allowed

Problems from previous competitions can be seen at http://www.verifythis.org

Submissions are to be sent by email to verifythis at cs.nuim.ie by the date indicated above.

PRIZES
The most suitable submission for competition will receive a prize.

ABOUT
VerifyThis 2017 will take place as part of the European Joint Conferences on Theory and Practice of Software (ETAPS 2017) on April 22-33, in Uppsala, Sweden. It is the 6th event in the VerifyThis competition series.

The aims of the competition are:
- to bring together those interested in formal verification, and to provide an engaging, hands-on, and fun opportunity for discussion
- to evaluate the usability of logic-based program verification tools in a controlled experiment that could be easily repeated by others.

The competition will offer a number of challenges presented in natural language. Participants have to formalize the requirements, implement a solution, and formally verify the implementation for adherence to the specification.

There are no restrictions on the programming language and verification technology used. The correctness properties posed in problems will have the input-output behaviour of programs in focus. Solutions will be judged for correctness, completeness and elegance.

ORGANIZERS
* Marieke Huisman, University of Twente, the Netherlands
* Rosemary Monahan, Maynooth University, Ireland
* Wojciech Mostowski, Halmstad University, Sweden
* Peter Müller, ETH Zürich, Switzerland
* Mattias Ulbrich, Karlsruhe Institute of Technology, Germany

CONTACT
Email: verifythis at cs.nuim.ie
Web: http://verifythis.ethz.ch