From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr 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 25D8D7EE51 for ; Fri, 19 Apr 2013 09:35:07 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of josr@itu.dk) identity=pra; client-ip=216.32.180.189; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="josr@itu.dk"; x-sender="josr@itu.dk"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of josr@itu.dk) identity=mailfrom; client-ip=216.32.180.189; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="josr@itu.dk"; x-sender="josr@itu.dk"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@co1outboundpool.messaging.microsoft.com) identity=helo; client-ip=216.32.180.189; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="josr@itu.dk"; x-sender="postmaster@co1outboundpool.messaging.microsoft.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AiQDANPycFHYILS9m2dsb2JhbABQDoI0erguiDSBHg4BAQEBAQYLCwkUCh6CIQEEAQEBD1seARomBwcyFAMQBAESCQsHAwSHcp5hDwJ2AQGKJQEBk1ONYYE9gmdhA5gqhG6FaodlP4FrAR4GGA X-IPAS-Result: AiQDANPycFHYILS9m2dsb2JhbABQDoI0erguiDSBHg4BAQEBAQYLCwkUCh6CIQEEAQEBD1seARomBwcyFAMQBAESCQsHAwSHcp5hDwJ2AQGKJQEBk1ONYYE9gmdhA5gqhG6FaodlP4FrAR4GGA X-IronPort-AV: E=Sophos;i="4.87,507,1363129200"; d="scan'208,217";a="13976838" Received: from co1ehsobe006.messaging.microsoft.com (HELO co1outboundpool.messaging.microsoft.com) ([216.32.180.189]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES128-SHA; 19 Apr 2013 09:35:05 +0200 Received: from mail27-co1-R.bigfish.com (10.243.78.233) by CO1EHSOBE011.bigfish.com (10.243.66.74) with Microsoft SMTP Server id 14.1.225.23; Fri, 19 Apr 2013 07:35:03 +0000 Received: from mail27-co1 (localhost [127.0.0.1]) by mail27-co1-R.bigfish.com (Postfix) with ESMTP id 8F3D68E0391; Fri, 19 Apr 2013 07:35:03 +0000 (UTC) X-Forefront-Antispam-Report: CIP:157.56.249.69;KIP:(null);UIP:(null);IPV:NLI;H:AMSPRD0210HT003.eurprd02.prod.outlook.com;RD:none;EFVD:NLI X-SpamScore: 1 X-BigFish: PS1(zzd79eh618I9feIc85ehzz1f42h1fc6h1ee6h1de0h1d18h1fdah1202h1e76h1d1ah1d2ahz70kz177df4h17326ah18c673h8275dh8275chz2dh2a8h668h839hd25he5bhf0ah1288h12a5h12bdh137ah1441h1504h1537h153bh162dh1631h1758h18e1h1946h19b5h1ad9h1b0ah1bceh1155h) Received: from mail27-co1 (localhost.localdomain [127.0.0.1]) by mail27-co1 (MessageSwitch) id 1366356851285573_29329; Fri, 19 Apr 2013 07:34:11 +0000 (UTC) Received: from CO1EHSMHS001.bigfish.com (unknown [10.243.78.243]) by mail27-co1.bigfish.com (Postfix) with ESMTP id 0B23B8401EA; Fri, 19 Apr 2013 07:33:56 +0000 (UTC) Received: from AMSPRD0210HT003.eurprd02.prod.outlook.com (157.56.249.69) by CO1EHSMHS001.bigfish.com (10.243.66.11) with Microsoft SMTP Server (TLS) id 14.1.225.23; Fri, 19 Apr 2013 07:33:53 +0000 Received: from AMSPRD0210MB354.eurprd02.prod.outlook.com ([169.254.7.3]) by AMSPRD0210HT003.eurprd02.prod.outlook.com ([10.255.63.166]) with mapi id 14.16.0293.003; Fri, 19 Apr 2013 07:33:51 +0000 From: Joseph Roland Kiniry To: "acl2@utlists.utexas.edu" , "afsec@afsec.asr.cnrs.fr" , "amast@cs.utwente.nl" , "calculemus-ig@mathweb.org" , "caml-list@inria.fr" , "comlab@comlab.ox.ac.uk" , "concurrency@listserver.tue.nl" , "coq-club@pauillac.inria.fr" , "event@in.tu-clausthal.de" , "events@fmeurope.org" , "fmcad@utlists.utexas.edu" , "gdr-im@gdr-im.fr" , "hol-info@lists.sourceforge.net" , "lics@research.bell-labs.com" , "lprolog@cs.umn.edu" , "matita@cs.unibo.it" , "mizar-forum@mizar.uwb.edu.pl" , "prog-lang@diku.dk" , "pvs@csl.sri.com" , "qpq-general@qpq.org" , "sal@csl.sri.com" , "strqds@laas.fr" , "theorem-provers@ai.mit.edu" , "theory-logic@cs.cmu.edu" , "theorynt@listserv.nodak.edu" , "yices@csl.sri.com" Thread-Topic: VSTTE Competition 2013: Final Announcement Thread-Index: AQHOPNA8cpIuHAT6U0a+0+y+rDU4MA== Date: Fri, 19 Apr 2013 07:33:51 +0000 Message-ID: Accept-Language: en-US Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: x-originating-ip: [10.255.63.132] Content-Type: multipart/alternative; boundary="_000_A859EE7B352948BDB1537F6A2D58DCE1itudk_" MIME-Version: 1.0 X-OriginatorOrg: itu.dk X-Validation-by: jkin@dtu.dk Subject: [Caml-list] VSTTE Competition 2013: Final Announcement --_000_A859EE7B352948BDB1537F6A2D58DCE1itudk_ Content-Type: text/plain; charset="Windows-1252" Content-Transfer-Encoding: quoted-printable Final Announcement VSTTE Competition 2013 http://www.vscomp.org/ 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 VSCom= p 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 the= ir implementations. Consequently, teams that competed in previous competitions are encouraged t= o recruit new team members whose skills complement those of the existing te= am members. For example, perhaps the current team is great at low-level de= sign and verification, but is weak in writing requirements or in rigorous validation/testing. The aims of the competition are: * to bring together those interested in rigorous software engineering and for= mal verification, and to provide an engaging, hands-on, and fun opportunity= for competition and mutual-learning, * to evaluate the usability of a variety of software engineering tools, not t= he least of which are logic-based program verification tools, in a controll= ed experiment that could be easily repeated by others. After the initial announcement of the contest we were asked the following q= uestion by more than one party. You=92ll 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 a= nd venues (e.g., ACM, ICFP, and TopCoder) to pay more attention to engineer= ing and quality, but to little effect. If we are going to see a contest li= ke this survive and even thrive in the long run, it seems it has to be an o= utgrowth of the verification community, rather than the implementation-cent= ric 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 wi= ll be decomposed for the contestants into an architecture, whose constituen= t pieces are the sub-problems of the contest. Thus, by solving all sub-pro= blems, one writes the entire application. What's more, the architecture is= specified in such a way that independent solutions to sub-problems submitt= ed 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 specification= s, implementation, validation, verification, and traceability. A well-prep= ared team will have a methodology prepared for each of these facets. The s= ubmission of a solution for a sub-problem need not include any of these fac= ets in particular---i.e., running, verified code is neither necessary nor s= ufficient 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 proce= ss are very welcome. There is no limit on team size, but the results will = be normalized by team size. We particularly encourage participation of: * student teams (this includes PhD students), * non-developer teams using a tool someone else developed, and * 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 correctnes= s, 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 point= s in each category available is indicated in parentheses: domain analysis (= 3), requirements (3), architecture (3), design (6), implementation (6), val= idation (6), formal verification (12), traceability (3). The maximum numbe= r of points available for each sub-problem is 42. The verification researc= her 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 expe= ct 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: * best team * best student team * 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 co= ntest problems will go live at this site at 9:00 GMT on Saturday the 20th o= f April. (Take note of your daylight savings time GMT offset!) There is no= need 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). --_000_A859EE7B352948BDB1537F6A2D58DCE1itudk_ Content-Type: text/html; charset="Windows-1252" Content-ID: Content-Transfer-Encoding: quoted-printable

Final An= nouncement

VSTTE Competition 2013=
20-22 April 2013 (NOTE: The f= irst announcement posted on 4 April had the wrong dates!)
Organizers: Joseph Kiniry, Ha= nnes Mehnert, Dan Zimmerman

This edition of the VSTTE pro= gramming contest is an experiment of a different kind, as it is more about software engineering than programmin= g.  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 mor= e than just verified data types and algorithms at the source code level.  Unlike previous competitions, t= his year's VSComp will focus on a rigorously
engineered software system= .  Contestants will be evaluated for all of the software engineering a= rtifacts that they produce, not just for verifying their implementations.

Consequently, teams that comp= eted in previous competitions are encouraged to recruit new team members whose skills complement those of the existing = team members.  For example, perhaps the current team is great at low-l= evel design and verification, but is weak in writing
requirements or in rigorou= s validation/testing.

The aims of the competition a= re:

  • to bring tog= ether those interested in rigorous software engineering and formal verifica= tion, and to provide an engaging, hands-on, and fun opportunity for competition and mutual-learning,
  • 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 easily repeated by others.=

After the initial announcemen= t of the contest we were asked the following question by more than one party.  You=92ll find it in our FAQ.

Q. Why attach this style of contest to VSTTE, if we are not focusing exclusiv= ely on verification?

A. Not a single international programming contest rewards good software engin= eering behavior.  We have tried for years to influence the big contest= s and venues (e.g., ACM, ICFP, and TopCoder) to pay more attention to engin= eering and quality, but to little effect.  If we are going to see a contest like this survive and even thrive i= n the long run, it seems it has to be an outgrowth of the verification comm= unity, 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 syst= em will be decomposed for the contestants into an architecture, whose const= ituent 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 indepe= ndent solutions to sub-problems submitted by competing teams should compose= into the final system.

The kinds of software enginee= ring concepts mentioned in the contest include: requirements, domain analysis, design, architecture, formal speci= fications, implementation, validation, verification, and traceability. &nbs= p;A well-prepared team will have a methodology prepared for each of these f= acets.  The submission of a solution for a sub-problem need not include any of these facets in particular---i.e= ., running, 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 an= alysis) 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 par= ticipation of:
  • student team= s (this includes PhD students),
  • non-develope= r teams using a tool someone else developed, and
  • several team= s using the same tool

A panel of judges will evalua= te contest entries to independently score sub-problems and determine the winner.  Solutions will be judge= d for correctness, completeness and elegance.  The total score for a s= ub-problem is the sum of its scores in the following categories, where the = total number of points in each category available is indicated in parentheses: domain analysis (3), requirements (3), archit= ecture (3), design (6), implementation (6), validation (6), formal verifica= tion (12), traceability (3).  The maximum number of points available f= or 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 ends so that contestants can comment upon each other's submissions= .  We expect that a paper will be co-authored by all interested contes= tants about the contest's results, as in several previous contests.<= /div>
The contest begins at 9:00 GM= T on Sat 20 April and ends at 9:00 GMT on Mon 22 April.

Prizes will be awarded in the= following categories:
  • best team
  • best student= team
  • tool used mo= st effectively by the most teams

The contests website is http://www.vscomp.org/.  You will find there momentarily an outline of the contest, a some Fr= equently Asked Questions.  The contest problems will go live at this s= ite at 9:00 GMT on Saturday the 20th of April.  (Take note of your day= light savings time GMT offset!) There is no need to pre-register for the contest, but you are welcome to warn us that you'l= l be competing.

Questions or comments about t= he contest should be sent to Joe Kiniry (kiniry@acm.org).
--_000_A859EE7B352948BDB1537F6A2D58DCE1itudk_--