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

Fwd: [Caml-list] VSTTE Competition 2013 Second Announcement

This year's competition (now finished) involved implementing a
verified DNS server.  I'm looking forward to seeing the submissions.


---------- Forwarded message ----------
From: Sam Owre <owre@xxxxxxxxxxx>
Date: 17 April 2013 21:17
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 wrong dates!)
Organizers: Joseph Kiniry, Hannes Mehnert, Dan Zimmerman

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, 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.

After the initial announcement of the contest we were asked the
following question by more than one party.  Youâll
find it in our FAQ.

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

A. Not a single international programming contest rewards good
software engineering behavior.  We have tried for
years to influence the big contests and venues (e.g., ACM, ICFP, and
TopCoder) to pay more attention to
engineering and quality, but to little effect.  If we are going to see
a contest like this survive and even thrive
in the long run, it seems it has to be an outgrowth of the
verification community, 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
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 traceability.  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

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:

  â 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 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 points in each category available is
indicated in parentheses: domain analysis (3), requirements (3),
architecture (3), design (6), implementation (6),
validation (6), formal verification (12), traceability (3).  The
maximum number 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 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 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
momentarily 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 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

Caml-list mailing list.  Subscription management and archives:
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs



Lists.xenproject.org is hosted with RackSpace, monitoring our
servers 24x7x365 and backed by RackSpace's Fanatical Support®.