ProofCompets/VSTTE2012

#概要 - 日時: 2011 11/09 0:00 - 11/10 24:00 (48H) - 送信先: - VSTTE 2012 compet 本家

#Call For Participations posted Sep 28, 2011 12:40 PM by Andrei Paskevich [ updated Oct 7, 2011 6:21 AM ]

A software verification competition is organized on behalf of the VSTTE 2012 conference. 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.

ソフトウェア検証競争とはVSTTEの支援により運営される。 競技の目的は: 方法やツールの進展を助けること、検証の新しい指標を与えること、開発者や検証者に刺激を与えること、楽しむことである。

The contest takes place during 48 hours, 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.

コンテストはカンファレンスの2ヶ月前の48時間、つまり2011年11月8日から10日まで行われる。問題はカンファレンスのウェブサイトに置かれるだろう。解は主催者へ電子メールで送らなければならない。どんなプログラミング言語、仕様記述言語、検証ツールを使っても構わない。

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 preferred to brevity. A certain degree of subjectivity in judgement 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, a given solution cannot appear in different submissions.

このコンテストには誰でも参加できる。チームでの作業も許される。4人までのチームだけが一等賞となる資格を持つ。参加者はいくつかのチームに属しても良い。しかし、同じ解が異なるsubmisionに現れてはいけない。

The technical requirements are as follows:

• access to the web to download the problems (a PDF file);
• access to the email to submit the solutions;
• any software used in the solutions should be freely available for non-commercial 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.

技術的な必要要件は以下のとおりである:

• 問題(PDFファイル)をダウンロードできるウェブアクセスができること
• 解を送るためのemailへアクセスできること
• 回答に使ったすべてのソフトウェアが非営利目的で自由に使えるように公開されていること。これはマイクロソフトの Z3のようなソースがクローズドなプログラムを除外しない。ソフトウェアはx86 LinuxまたはWindowsマシンで使えなければならない。参加者はコンペの間にそれらのツールを修正することは認められる。

##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:

submission は(可能なら圧縮された)tarballで、(例えばチーム名の名前が付いた)一つのディレクトリを含む。このディレクトリはREADMEという名前のテキストファイルを少なくとも持ち、解いた問題ごとにディレクトリを含める。つまり、次のような感じになる:

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.

READMEファイルは次の情報をもっていなければならない:

• コンタクト情報(email)
• 回答の詳細の記述: specifyされた(かつ/または)証明された性質、制限(かつ/または)一般化、その他のレビューを促進させるかもしれない情報
• 使用するソフトウェア、それを得るURL、コンパイルコマンドなどを含む、回答をリプレイする詳細の説明

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 (University 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.