VSTTE 2012 Verification Competition ----------------------------------- A software verification competition is organized on behalf of the VSTTE 2012 conference (https://sites.google.com/site/vstte2012). The purposes of this competition are: to help promote approaches and tools, to provide new verification benchmarks, to stimulate further development of verification techniques, and to have fun. The contest takes place during two days, 17-19 November 2011, two months prior to the conference. Problems will be put on the website of the conference. Solutions must be sent by email to the competition organizers. Any programming language, specification language, and verification tool is allowed. Problems -------- There will be several, independent problems. Each problem is presented as an algorithm, using English or pseudocode, and a list of properties to formally prove about it, also expressed in plain English and standard mathematical notation. Evaluation ---------- Submissions are ranked according to the total sum of points they score. Each problem includes several sub-tasks, e.g. safety, termination, behavioral correctness, etc., and each sub-task is given a number of points. While evaluating the submissions, judges take into account the accuracy and thoroughness of solutions as well as their terseness and elegance. A certain degree of subjectivity is inevitable and should be considered as part of the game. Participants ------------ Anybody interested can take part in the contest. Team work is allowed. However, only teams up to 4 members are eligible for the first prize. The technical requirements are as follows: - access to the web to download the problems (PDF file); - access to the email to submit the solutions; - any software used in the solutions should be freely available to the public (this does not exclude closed source programs such as Microsoft's Z3) and usable on an x86 Linux or Windows machine. Submission ---------- A submission is a (possibly compressed) tarball that contains exactly one directory (named by the team, for instance). This directory should contain at least a text file named README, and one directory for each problem solved. Thus it must look like: team/ -+ +- README +- problem1/ +- problem2/ + ... +- problemN/ +- other stuff... The README file should contain the following information: - contact information (email); - detailed description of the submitted solutions: properties that have been specified and/or proved, restrictions and/or generalizations, anything that may facilitate the review; - detailed instructions to replay the solutions, including the software to use, URLs to get it from, compilation commands, etc. Organizers ---------- - Jean-Christophe Filliâtre (CNRS, France) - Andrei Paskevich (Univ Paris Sud, France) - Aaron Stump (University of Iowa, USA) Schedule -------- Thursday 17 Nov 2011, 15:00 UTC - competition starts Saturday 19 Nov 2011, 15:00 UTC - competition stops Monday 12 Dec 2011 - the winner is notified 28-29 Jan 2012 - results are announced at VSTTE 2012 Prize ----- The winner is awarded a talk slot at VSTTE 2012, to present any research of his/her choice of interest for the VSTTE community. In particular, a presentation of solutions to the competition problems and/or of the techniques and system used would be appreciated. -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.