From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id 752827EE51 for ; Wed, 17 Apr 2013 22:17:16 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of owre@csl.sri.com) identity=pra; client-ip=128.18.84.132; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="owre@csl.sri.com"; x-sender="owre@csl.sri.com"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of owre@csl.sri.com) identity=mailfrom; client-ip=128.18.84.132; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="owre@csl.sri.com"; x-sender="owre@csl.sri.com"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@brightmail-internal3.sri.com) identity=helo; client-ip=128.18.84.132; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="owre@csl.sri.com"; x-sender="postmaster@brightmail-internal3.sri.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: ApMBAG0Cb1GAElSEnGdsb2JhbABQgzyDMbh6hR4WDgEBAQEBBg0JCRQoghcySjkIAgUhAhE6GgEMCQsHA4VYgh6cKI5Skl0VgQ6MQINxgRMDiQaiP4FLAR4G X-IPAS-Result: ApMBAG0Cb1GAElSEnGdsb2JhbABQgzyDMbh6hR4WDgEBAQEBBg0JCRQoghcySjkIAgUhAhE6GgEMCQsHA4VYgh6cKI5Skl0VgQ6MQINxgRMDiQaiP4FLAR4G X-IronPort-AV: E=Sophos;i="4.87,495,1363129200"; d="scan'208";a="13746730" Received: from brightmail-internal3.sri.com ([128.18.84.132]) by mail2-smtp-roc.national.inria.fr with ESMTP; 17 Apr 2013 22:17:14 +0200 X-AuditID: 80125484-b7fa56d000006ee0-2d-516f03487ee2 Received: from mx0.csl.sri.com (mx0.csl.sri.com [130.107.1.30]) (using TLS with cipher AES256-SHA (AES256-SHA/256 bits)) (Client did not present a certificate) by brightmail-internal3.sri.com (SRI Internal SMTP Gateway) with SMTP id AE.1C.28384.9430F615; Wed, 17 Apr 2013 13:17:13 -0700 (PDT) Received: from ubi (ubi.csl.sri.com [130.107.15.8]) by mx0.csl.sri.com (8.14.3/8.14.2) with ESMTP id r3HKH7mT033233 (version=TLSv1/SSLv3 cipher=AES256-SHA bits=256 verify=NO); Wed, 17 Apr 2013 13:17:08 -0700 (PDT) (envelope-from owre@csl.sri.com) Received: from owre (helo=ubi) by ubi with local-esmtp (Exim 4.72) (envelope-from ) id 1USYmx-0007gO-Fz; Wed, 17 Apr 2013 13:17:07 -0700 To: Undisclosed recipients: ; X-Mailer: MH-E 8.2; nmh 1.3; GNU Emacs 23.1.1 MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable Date: Wed, 17 Apr 2013 13:17:07 -0700 Message-ID: <29535.1366229827@ubi> From: Sam Owre X-Brightmail-Tracker: H4sIAAAAAAAAA02Ra0hTYQCG/XbO2Y7S6jglP2+BIxE0LZ3FF5T0I+QLjBRCIgNbedLl3ORs StpteQmdiLeKpuK1bKmoGaZZWY68Rm2agooZkmJoMq9pXkbqEPz38L4vz5+XJkQjpAstU6hZ TiGVi/l2ZEosOOR7jlCGHVsYIFFHy0uAimu7KTRkVCBNUztACy0NJJprbKPQmukbhaZ0egLV LA3xUM7wxNZsc5xAOb2LAjTdV0SivMoHAGUZMFqefSJAS13BSD+5RqDFF4MUylp3R69n9QK0 XFVKodbRKgF6t9Gz5Zmf5iFDAYn6/rznn3HFq9oBEmd0q3FTeheJh3ODcNnnENyrKePjRz9S CLw6U0/h2twVgDffXsKWggoSd3amE1hb4IDzfxtIrFttAbi186Mg1Pmy3akoVi5LZLmjQVft Yizrp+ONvrdGih4KNCDTUwtsacgEwva2OYGVD0LTWD1fC+xoEVPNg9qFDGq7EDEWAN80A2vx FMCGonaeFtC0I+MON4zcNjowEvhr0dvq8YXzFbodp5Cxhz26CXKbCcYLbpT0E1b2gVXlMztM Mp5wY7COsu7FML80YyfnMx4wdaScyAX7C/eoCveoCveoygBRDdyucbLoGHWcVCb33f1Z4qfi ZH7XlXGNYOtxjehiWgvQt/obAEMD8T7hyS+HQ0WUNFGVFGcAkCbEjsL7rxRhImGUNCmZ5ZSR XIKcVRmAK02KnYThkgMXREy0VM3Gsmw8y+22PNrWRQNKjPf0lHDdxmTk31157hjkU8WM394s tslzSv00WRjiNJbQf+XD19mOykHXiDuipWYvxfdmtwhzGpmpbFRmwHoP4ohBUiPoszwOCB2N +KcuDp6PdD/RfzZr5G9gsvfxZ8n2N87XmuWr/W6qgJtsqSk73FxHm43ZP5d4U846S6mYVMVI /b0JTiX9D0sYMnrtAgAA Subject: [Caml-list] VSTTE Competition 2013 Second Announcement Second Announcement VSTTE Competition 2013 20-22 April 2013 (NOTE: The first announcement posted on 4 April had the wr= ong dates!) Organizers: Joseph Kiniry, Hannes Mehnert, Dan Zimmerman This edition of the VSTTE programming contest is an experiment of a differe= nt kind, as it is more about software engineering than programming. It is not a contest to see who can write and= verify small problems as quickly as possible, but instead how can a team create a quality piece of code, using = any tools and techniques (not just verification), in a short period of time. Quality software is about more than just verified data types and algorithms= at the source code level. Unlike previous competitions, this year's VSComp will focus on a rigorously engineered software system. Contestants will be evaluated for all of the s= oftware engineering artifacts that they produce, not just for verifying their implementations. Consequently, teams that competed in previous competitions are encouraged t= o recruit new team members whose skills complement those of the existing team members. For example, perhaps the cu= rrent team is great at low-level design and verification, but is weak in writing requirements or in rigorous validation/testing. The aims of the competition are: =E2=80=A2 to bring together those interested in rigorous software enginee= ring and formal verification, and to provide an engaging, hands-on, and fun opportunity for competition and mutual-lear= ning, =E2=80=A2 to evaluate the usability of a variety of software engineering = tools, not the least of which are logic-based program verification tools, in a controlled experiment that could be ea= sily repeated by others. After the initial announcement of the contest we were asked the following q= uestion by more than one party. You=E2=80=99ll find it in our FAQ. Q. Why attach this style of contest to VSTTE, if we are not focusing exclus= ively on verification? A. Not a single international programming contest rewards good software eng= ineering behavior. We have tried for years to influence the big contests and venues (e.g., ACM, ICFP, and TopCod= er) to pay more attention to engineering and quality, but to little effect. If we are going to see a co= ntest like this survive and even thrive in the long run, it seems it has to be an outgrowth of the verification com= munity, rather than the implementation-centric hack-fast community. The contest takes place over a two-day period. The system that contestants= must develop is secret until the moment the contest starts. The system will be decomposed for the contestan= ts into an architecture, whose constituent pieces are the sub-problems of the contest. Thus, by solving a= ll sub-problems, one writes the entire application. What's more, the architecture is specified in such a way that= independent solutions to sub-problems submitted by competing teams should compose into the final system. The kinds of software engineering concepts mentioned in the contest include= : requirements, domain analysis, design, architecture, formal specifications, implementation, validation, ve= rification, and traceability. A well-prepared team will have a methodology prepared for each of these facet= s. The submission of a solution for a sub-problem need not include any of these facets in particular---i.e., runn= ing, verified code is neither necessary nor sufficient to win the contest. There are no restrictions on concepts, tools, and technologies used. Teams = whose focus in on "early" (i.e., requirements or domain analysis) or "late" (validation/testing or evolution= ) phases of the software engineering process are very welcome. There is no limit on team size, but the results = will be normalized by team size. We particularly encourage participation of: =E2=80=A2 student teams (this includes PhD students), =E2=80=A2 non-developer teams using a tool someone else developed, and =E2=80=A2 several teams using the same tool A panel of judges will evaluate contest entries to independently score sub-= problems and determine the winner. Solutions will be judged for correctness, completeness and elegance. The = total score for a sub-problem is the sum of its scores in the following categories, where the total number of po= ints in each category available is indicated in parentheses: domain analysis (3), requirements (3), architectu= re (3), design (6), implementation (6), validation (6), formal verification (12), traceability (3). The maximum nu= mber of points available for each sub-problem is 42. The verification researcher will note the weight given = to formal verification. All submitted artifacts will be made public immediately after the contest e= nds so that contestants can comment upon each other's submissions. We expect that a paper will be co-authored = by all interested contestants about the contest's results, as in several previous contests. The contest begins at 9:00 GMT on Sat 20 April and ends at 9:00 GMT on Mon = 22 April. Prizes will be awarded in the following categories: =E2=80=A2 best team =E2=80=A2 best student team =E2=80=A2 tool used most effectively by the most teams The contests website is http://www.vscomp.org/. You will find there moment= arily an outline of the contest, a some Frequently Asked Questions. The contest problems will go live at this site= at 9:00 GMT on Saturday the 20th of April. (Take note of your daylight savings time GMT offset!) There is no n= eed to pre-register for the contest, but you are welcome to warn us that you'll be competing. Questions or comments about the contest should be sent to Joe Kiniry (kinir= y@acm.org).