VSTTE 2012 Solutions using ACL2

The VSTTE 2012 competition took place November 8-10, 2011, over 48 hours. Roughly 40 teams (of up to four people per team) entered solutions, which were then scored by a panel of judges. A total of 600 points were possible. The winners, announced at the Verified Software: Theories, Tools and Experiments conference held January 28-29, 2012 in Philadelphia, USA, were:

Gold medal (600 points):
- Team "acl2-dkms": Jared Davis, Matt Kaufmann, J Strother Moore, and Sol Swords with ACL2.
- Team "KIV": Gidon Ernst, Gerhard Schellhorn, Kurt Stenzel, and Bogdan Tofan using KIV.
Silver medal (595 points):
- Team "LeinoMueller": K. Rustan M. Leino and Peter Müller with Dafny.
- Team "SRI": Sam Owre and Natarajan Shankar using PVS.
Bronze medal (590 points):
- Team "eam": Ernie Cohen and Michał Moskal with VCC.
- Team "JasonAndNadia": Jason Koenig and Nadia Polikarpova with Dafny.

Here we provide links to:

The problems (a local copy, originally from https://sites.google.com/site/vstte2012/compet/problems/)

A directory containing the ACL2 team's solutions to all parts of the five problems using ACL2 Version 4.3. See also the README file in that directory.

A gzipped tarball for the above directory

We are especially grateful to Centaur Technology, the employer of team members Jared Davis and Sol Swords, which graciously allowed them to focus on this exercise during the competition. We are also grateful to those who worked so hard to pose the problems so clearly and those who judged the submissions.