Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] VSTTE 2012 Verification Competition: last call for participation

  • Subject: [Frama-c-discuss] VSTTE 2012 Verification Competition: last call for participation
  • From: andrei at lri.fr (Andrei Paskevich)
  • Date: Wed, 2 Nov 2011 13:58:21 +0100
VSTTE 2012 Verification Competition starts Tuesday 8 November 2011!
Follow the announcements at the competition Web page:

    https://sites.google.com/site/vstte2012/compet

Join the discussion group or subscribe to our mailing list:

    http://groups.google.com/group/vstte-2012-verification-competition

    vstte-2012-verification-competition+subscribe at googlegroups.com


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 48 hours, on 8-10 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 a sequential algorithm, using English or pseudocode, and
a list of properties to formally prove about it, also expressed in
plain English and standard mathematical notation. Participants have
liberty to implement the proposed algorithms in functional,
imperative, object-oriented, or any other programming style.


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. ?(Clarity is more important than brevity.)
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.
Only teams up to 4 members are eligible for the first prize.
Individual participants may belong to several teams.
However, the same solution cannot appear in different submissions.

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 for
noncommercial use to the public. This does not exclude closed source
programs (such as Microsoft's Z3). Software must be usable on an x86
Linux or Windows machine. Participants are authorized to modify
their tools during the competition.


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.

Several solutions can be submitted for the same problem (for instance,
using different tools). They should be stored in separate subdirectories
of problemI/. During evaluation, only the best-faring solution will be
taken into account.


Organizers
----------
- Jean-Christophe Filli?tre (CNRS, France)
- Andrei Paskevich (Univ Paris Sud, France)
- Aaron Stump (University of Iowa, USA)


Schedule
--------
Tuesday ? 8 Nov 2011, 15:00 UTC - competition starts
Thursday 10 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.