[ecoop-info] CALL FOR PROBLEMS: VerifyThis Verification Competition 2012

[Vladimir Klebanov]

****************************************
VerifyThis Verification Competition 2012

          CALL FOR PROBLEMS

Competition to be held at FM 2012
30-31 August 2012, Paris, France

http://fm2012.verifythis.org/
****************************************

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



IMPORTANT DATES

Submission deadline: August 6, 2012
Competition: August 30-31, 2012



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 especially welcome
- the organizers reserve the right (but no obligation) to use the
  problems in the competition, either as submitted or with modifications
- after the competition, submitted problems (and solutions) will be
  published on verifythis.org
- submissions from (potential) competition participants are allowed

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

Submissions are to be sent per email to fm2012 at verifythis.org by the
date indicated above.


PRIZES

The best submission will receive a prize.



ABOUT

VerifyThis is a two-day event taking place as part of the Symposium on
Formal Methods (FM 2012) on August 30-31 in Paris, France. It is a
successor of the program verification competition held at FoVeOOS 2011.

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 behavior of programs in focus. Solutions will be judged
for correctness, completeness and elegance.

Registration to participate in the competition is open (see website).



ORGANIZERS

* Marieke Huisman, University of Twente, the Netherlands
* Vladimir Klebanov, Karlsruhe Institute of Technology, Germany
* Rosemary Monahan, National University of Ireland Maynooth



CONTACT

fm2012 at verifythis.org
http://fm2012.verifythis.org/


-- 
Vladimir Klebanov
Postdoctoral Researcher, Application-oriented Formal Verification
Karlsruhe Institute of Technology
http://formal.iti.kit.edu/~klebanov