[SAL] VSTTE Informal Verification Competition

Natarajan Shankar shankar at csl.sri.com
Fri Jul 16 09:01:32 PDT 2010

Dear colleague:

We will have an informal verification competition at VSTTE in Edinburgh
as a prelude to a more formal competition at future meetings.  The
competition is for teams of up to three people armed with one or more
verification tools.  You will be given several verification
exercises with information specifications, test cases, and pseudocode.
The task is to prepare a reproducible verification of executable code
relative to a formalization of the specifications.  The results will be
judged for completeness and elegance.  The exercises will typically
involve simple datatypes that should be available on most verification
tools for sequential or functional programs.  Student teams are
especially encouraged.  

We also urge you to register for VSTTE itself (see the Call below).  The
competition will be an informal event, no registration is required. If
you want to participate, simply attend the session on Wednesday Aug 18
and find out about the details.  The results will be presented at the
Tools & Experiments workshop on Thu Aug 19.  More information should
also be available on the VSTTE web page shortly.

Please contact peter.mueller at inf.ethz.ch or shankar at csl.sri.com
if you have any questions.

We look forward to seeing you at VSTTE!

Peter and Shankar


(Apologies if you receive multiple copies of this announcement)


          *** Second Call for Participation -- Early Registration ends in 2 weeks ***

Third International Conference on Verified Software:
             Theories, Tools, and Experiments

                 Edinburgh, Scotland

               August 16th-19th, 2010


SPONSORS: NSF, EPSRC, Microsoft Research, SICSA, Altran Praxis,
         SSEI, FME, Contemplate, Heriot-Watt University


The Third International Conference on Verified Software: Theories,
Tools, and Experiments follows a successful inaugural working
conference at Zurich (2005) and a successful conference in Toronto
(2008). This conference is part of the Verified Software Initiative
(VSI), a fifteen-year, cooperative, international project directed
at the scientific challenges of large-scale software verification.
VSI also includes UKCRC's Grand Challenge 6, i.e. Dependable Systems

The programme includes 
  - Keynote presentations by Tom Ball (Microsoft), Gerwin Klein (National ICT Australia), and
    Matthew Parkinson (University of Cambridge); 
  - Invited Tool Demo Presentations by Colin O?Halloran (ClawZ/Circus) , Bart Jacobs (VeriFast), 
    Michael Jastram (ProB) and Joe Kinry (BONc/Beetlz);
  - A Verification Competition;
  - Industrial Tool Vendors;
  - Two workshops: Theory WS and Tools & Experiments WS;
  - A Summer School -- lectures given by Robert Atkey/Ewen Maclean, Alan Bundy/Lucas Dixon, 
    Jane Hillston, Cliff Jones, Gerwin Klein, J Strother Moore, Natarajan Shankar and Graham Steel;
A provisional programme is available at:


VSTTE 2010 is being hosted by Heriot-Watt University in Edinburgh.
The conference dates coincide with the 2010 Edinburgh International
Festival and the Edinburgh Festival Fringe -- collectively the
largest annual arts festival on the planet! The technical programme
will take place in the Edinburgh Conference Centre (Heriot-Watt University 
campus), where accommodation will be available at very competitive rates for
festival time. Social events will be arranged within the city centre,
making VSTTE an unique cultural and scholarly event for 2010!

As well as a welcome reception and conference banquet, SICSA are
sponsoring a special drinks reception in the Informatics Forum 
at the heart of the Festival on August 17th. 

Support for students wishing to attend VSTTE 2010 is available. 
Please contact vstte10 at macs.hw.ac.uk for more details. 

Online registration is available from


Early registration ends on July 31st. 

More information about the SAL mailing list