Competition

Organisers: Natarajan Shankar and Peter Mueller

There will be an informal verification competition during the conference as a prelude to a more formal competition at future meetings.  The rules of the game are as follows:

1. •The competition is for teams of up to three people armed with one or more verification tools.
   

2. •The team will be given several verification exercises with informal specifications, test cases, and pseudocode. These will be provided at the last session of the main conference, at 12:00-12:30 on Wednesday 18th August.
   

3. •The task is to prepare a reproducible verification of executable code relative to a formalization of the specifications. The teams have 2 hours to complete this experiment: 16:00-18:00 on Wednesday. The result has to be submitted to the organisers by 18:00 (more details on the submission details will be given in due course)
   

4. •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.  
   

5. •The competition will be an informal event, no registration is required. If you want to participate, simply attend the session on Wednesday 18th August and find out about the details.
   

6. •Student teams are especially encouraged.
   

7. •The announcement of the result will be at the end of the TOOLS & EXPERIMENTS workshop on Thursday 19th August.
   

Click here to download the slides describing the competition.

Click here to download the competition solutions.

Click here to download additional solutions that we received after the competition.

A summary of the solutions is available is available from here.

Further discussion are encouraged and should be posted on http://verifythis.cost-ic0701.org/.