[isabelle] VerifyThis 2015: Final Call for Challenges


VerifyThis Verification Competition 2015
  Competition to be held at ETAPS 2015
 12 April 2015, London, UK
 Get involved, even if you cannot participate in the competition: provide
 a challenge.
  Submission deadline: November 28, 2014
 Competition: April 12, 2015

  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 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 at verifythis.org by the
 date indicated above.
  The best submission will receive a prize.
  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
 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 at verifythis.org.
  * Marieke Huisman, University of Twente, the Netherlands
 * Vladimir Klebanov, Karlsruhe Institute of Technology, Germany
 * Rosemary Monahan, Maynooth University, Ireland


 etaps2015 at verifythis.org

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.