From: Rosemary.Monahan@nuim.ie
VerifyThis Verification Competition 2015
FIRST ANNOUNCEMENT AND CALL FOR PROBLEMS
Competition to be held at ETAPS 2015
12 April 2015, London, UK
http://etaps2015.verifythis.org/
Get involved, even if you cannot participate in the competition: provide
a challenge.
IMPORTANT DATES
Submission deadline: November 28, 2014
Competition: April 12, 2015
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
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 especially welcome
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 per email to etaps2015@verifythis.org by the
date indicated above.
PRIZES
The best submission will receive a prize.
ABOUT
VerifyThis 2015 will take place as part of the European Joint
Conferences on Theory and Practice of Software (ETAPS 2015) on April
12th, 2015 in London, UK. It is the 4th 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.
Registration details are forthcoming. Informal inquiries are welcome at
etaps2015@verifythis.org.
ORGANIZERS
* Marieke Huisman, University of Twente, the Netherlands
* Vladimir Klebanov, Karlsruhe Institute of Technology, Germany
* Rosemary Monahan, Maynooth University, Ireland
CONTACT
etaps2015@verifythis.org
http://etaps2015.verifythis.org/
Last updated: Nov 21 2024 at 12:39 UTC