VerifyThis Verification Competition
held at FM 2012 in Paris
30-31 August 2012
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. A separate call for problem contributions is forthcoming.
Thursday, August 30th
12.30 - 12.40 verification competition presentation (at FM plenary session)
14.00 - 18.30 problem-solving session (Hall 02, Access 30, Level -1)
Friday, August 31st
10:30 - 12:30 Q&A session with participants and judges (Hall 02, Access 30, Level -1)
16:30 announcement of preliminary results (at FM closing session)
Participation is open for anybody interested. Teams of up to two people are allowed. Physical presence on site is required. We particularly encourage participation of:
- student teams (this includes PhD students)
- non-developer teams using a tool someone else developed
- several teams using the same tool
The competition is a satellite event of FM 2012. Participants must register on the FM website AND send an email to firstname.lastname@example.org listing team composition and tools. If you are registering for the main program of the FM, then access to the competition is included. You can also register for the competition alone: on the registration website, select "Two Days" from the drop-down menu titled "Workshop / Tutorial / Colocated event" and then select "Verification Competition" from the drop-down menu three lines down (the last one).
Prizes will be awarded in the following categories:
- best team
- best student team
- tool used by most teams
- distringuished user-assistance tool feature
To extend the problem pool and tender better to the needs of the participants, we are now soliciting verification problems for the competition:
- 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 www.verifythis.org.
Submissions are to be sent per email to email@example.com.
The best submission will receive a prize.
VerifyThis 2012 is a successor of the COST IC0701 Verification Competition held at FoVeOOS 2011. Similar past events are the 1st and the 2nd Verified Software Competitions held at VSTTE 2010 and on-line in the run-up to VSTTE 2012 respectively.
VerifyThis is also a collection of verification problems (and solutions). Its counterpart is VerifyThus - a distribution of deductive verification tools for Java-like languages, bundled and ready to run in a VM. Both were created with support from COST Action IC0701.
A workshop on comparative empirical evaluation of reasoning systems (COMPARE2012) was held on June 30th at IJCAR 2012 in Manchester. Competitions are one of the main topics of the workshop.