The 1st Verified Software Competition was organized by Peter Müller and Natarajan Shankar and held on 18 August 2010 at VSTTE 2010 in Edinburgh.

This page offers information and resources related to the competition:

A shortened version of the experience report has appeared in proceedings of FM 2011 (BiBTeX):
V. Klebanov, P. Müller, N. Shankar, G. T. Leavens, V. Wüstholz, E. Alkassar, R. Arthan, D. Bronish, R. Chapman, E. Cohen, M. Hillebrand, B. Jacobs, K. R. M. Leino, R. Monahan, F. Piessens, N. Polikarpova, T. Ridge, J. Smans, S. Tobies, T. Tuerk, M. Ulbrich, and B. Weiß. The 1st Verified Software Competition: Experience report. In M. Butler and W. Schulte, editors, Proceedings, 17th International Symposium on Formal Methods (FM), 2011.

The report has won the Best Paper Award from FM 2011.


The solution archive currently contains solutions produced with the following tools (both during the competition and for the FM paper):

Boogie (intermediate language with assertions)
Dafny (object-based language with built-in spec, like Java+JML)
HOL4 (functional impl., spec in HOL)
Holfoot (Separation logic for a C-like language, encoded in HOL)
Isabelle/VCG (Hoare logic for C0)
KeY (Dynamic logic for Java)
ProofPower (functional impl., spec in HOL)
Resolve (imperative component programs w/ modular specs)
SPARK/Ada (contractualized subset of Ada)
VCC (C with VCC assertions/invariants)
VeriFast (Separation logic for Java and C)

Since FM 2011 the following solutions have been submitted and (mostly) added to the archive:

PVS (not yet in the archive)
SPARK (new solutions)
Why3

ċ
solutions.zip
(1722k)
Vladimir Klebanov,
Jun 29, 2011, 6:06 AM
Ċ
Vladimir Klebanov,
Jun 22, 2011, 3:15 AM
Ċ
Vladimir Klebanov,
Jun 22, 2011, 3:13 AM
ċ
vscomp2010.bib
(1k)
Vladimir Klebanov,
Jun 22, 2011, 3:19 AM