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 7BA7F7EE5B for ; Wed, 3 Apr 2013 18:55:36 +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: AtUCADxeXFGAElSEnGdsb2JhbABDDoMvqw2WQRYOAQEBAQEICwkJFAoegiEGAQFqOQ8lDzoVEhsDh3YMwEAVjTcJhQsDiHqPEJI4X4FKAh4G X-IPAS-Result: AtUCADxeXFGAElSEnGdsb2JhbABDDoMvqw2WQRYOAQEBAQEICwkJFAoegiEGAQFqOQ8lDzoVEhsDh3YMwEAVjTcJhQsDiHqPEJI4X4FKAh4G X-IronPort-AV: E=Sophos;i="4.87,402,1363129200"; d="scan'208";a="11640359" Received: from brightmail-internal3.sri.com ([128.18.84.132]) by mail2-smtp-roc.national.inria.fr with ESMTP; 03 Apr 2013 18:55:35 +0200 X-AuditID: 80125484-b7fa56d000006ee0-47-515c5f05a49f 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 AB.E9.28384.50F5C515; Wed, 3 Apr 2013 09:55:33 -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 r33GtSDJ084175 (version=TLSv1/SSLv3 cipher=AES256-SHA bits=256 verify=NO); Wed, 3 Apr 2013 09:55:28 -0700 (PDT) (envelope-from owre@csl.sri.com) Received: from owre (helo=ubi) by ubi with local-esmtp (Exim 4.72) (envelope-from ) id 1UNQy8-0003KL-29; Wed, 03 Apr 2013 09:55:28 -0700 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 X-Mailer: MH-E 8.2; nmh 1.3; GNU Emacs 23.1.1 Date: Wed, 03 Apr 2013 09:55:27 -0700 Message-ID: <12792.1365008127@ubi> From: Sam Owre X-Brightmail-Tracker: H4sIAAAAAAAAA+NgFmpikeLIzCtJLcpLzFFi42JpymaU02WNjwk0eHlE0eLojpWMFnPWnGC1 uHE+z6Jh60FGi087NrBYfNi0j9Xi14VzrBbPZ65gtlj95QaTRf/NJ0Blfx8yW/Sf+sxu8eri bBaL7kMeFl/fTmO3+HLczWLF01/MFt2/ZS02v13BbvF12XxWi113lrFb7P5zEqj74ysmB3GP H11XWDw6TpR43Jxg57HgiI/HqYYFbB5T7jYxe/x4vZ7VY82E74wef3dGePybvIjFo2uysMek F4dYPGb+2MHosXvBZyaPKa8msnnc2dPCEiAWxWWTkpqTWZZapG+XwJXx//8y5oJj2hVPTu9m b2C8rtzFyMkhIWAi8aDlEiOELSZx4d56ti5GLg4hgVVMEluevGACSQgJ/GWUOLVWAiIxg1Fi /64PzCCOiMAhVokXLXvYQaqEBeQlJl9cyQYxSlfi46KZQHEODhYBVYm+f2ogYV4BJYm2H9NZ QWw2AUWJ5lsLmScwci9gZFjFKJNUlJmeUZKbmJmjC4sPY73ioky95PzcTYzAmGkQCmnZwbhi l+EhRgEORiUeXsvTKgFCrIllxZW5hxglOJiVRHinusQECvGmJFZWpRblxxeV5qQWH2KU5mBR EucNM+b3FxJITyxJzU5NLUgtgskycXBKNTCuqS5ZtHzfRk1N8WkTS9y8DDYLVyiaP3rtsWuP OtuD3ry9jl3v7LTaF89brc74NPlM0oabT28cPKW1dpXFvMaSyBa3ibwVm8JkGVlYzqzgzysL WRvT9fTti85tLwM2Tk54tit5dZx/SdzNWSnizy6cuN91O/oec363c+wBuaqqj0v7sx7nBAQp sRRnJBpqMRcVJwIAZtwMDZUCAAA= Subject: [Caml-list] VSTTE Competition 2013 VSTTE Competition 2013 19-21 April 2013 Organizers: Joseph Kiniry, Hannes Mehnert, Radu Grigore This edition of the VSTTE programming contest is an experiment of a different 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 [1], this year's VSComp will focus on a rigorously engineered software system. Contestants will be evaluated for all of the software engineering artifacts that they produce, not just for verifying their implementations. Consequently, teams that competed 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-level design 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 formal 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 the least of which are logic-based program verification tools, in a controlled experiment that could be easily repeated by others. The contest takes place over a three day period. The system that contestants must develop is secret until the moment the contest starts. The system will be decomposed for the contestants into an architecture, whose constituent pieces are the sub-problems of the contest. Thus, by solving all 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, verification, and traceablity. A well-prepared team will have a methodology prepared for each of these facets. 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 analysis) or "late" (validation/testing or evolution) phases of the software engineering process are very welcome. Teams must be of six contestants or less. 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 score sub-problems and determine the winner. Solutions will be judged for correctness, completeness and elegance. 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 contestants about the contest's results, as in several previous contests. The contest begins at 9:00 GMT on 19 April and ends at 23:39 on 21 April. Prizes will be awarded in the following categories: - best team - best student team - tool used most effectively by the most teams Questions or comments about the contest should be sent to Joe Kiniry (kiniry@acm.org). --- [1] Past VSComp Competitions Summary The first edition of the competition was a half-day live contest that took place at VSTTE in August 2010 and was organized by Shankar and Peter. Small teams focused on simple algorithms specified via natural language and pseudo-code. The algorithms were sum & max, inverting an injection, searching a linked list, the N-Queens problem, and an amortized queue. http://www.macs.hw.ac.uk/vstte10/Competition.html The 2011 competition was organized by Marieke, Vladimir, and Rosemary. It was a live competition that took place over a half day in October 2011 at FoVeOSS 2011. Small teams focused on simple algorithms specified using Java code. The algorithms were max of an array, max of a tree, finding two duplets in an array, and deciding on the cyclicity of a list. http://foveoos2011.cost-ic0701.org/verification-competition The 2012 VSTTE competition was organized by Jean-Christophe, Andei, and Aaron and was an online competition that took place over a 48 hour period in November 2011. It focused on somewhat more advanced algorithms than earlier competitions including two-way sort, an S & K combinator interpreter, a queue implemented with a ring buffer, tree reconstruction, and breadth-first search. https://sites.google.com/site/vstte2012/compet The VerifyThis competition was a two day affair that took place at FM 2012. It was organized by Marieke, Vladimir, and Rosemary. Teams of up to two people focused on three problems: longest common prefix of two arrays, prefix sum of an array, and iterative deletion in a binary search tree. http://fm2012.verifythis.org/