VerifyThis 2012
VerifyThis 2012 was organized by Marieke Huisman, Vladimir Klebanov, Rosemary Monahan.
The competition report can be found here (PDF, 496 KB).
Winners
The main results of the competition are as follows:
- Best team: Bart Jacobs, Jan Smans (VeriFast)
- Best student team: Gidon Ernst, Jörg Pfähler (KIV)
- Distinguished user-assistance tool feature: integration of proving
and run-time assertion checking in GNATprove (team member: Yannick
Moy)
- Tool used by most teams: prize shared between Dafny and Why3
- Best (pre-competition) problem submission: “Optimal Replay” by
Ernie Cohen
Challenges
Competition challenges will be posted here. Tentative schedule for
August 30th:
Solutions
Below are the solutions developed by participants during and after the
competition. Solutions may be updated as time goes on. The date
indicates last modification of the uploaded files or the link and can be
approximate.
RULES
- Solutions are to be submitted per email
- Submissions must state the version of the verification system used
(for development versions, internal revision, timestamp, or similar
unique id).
- The main rule of the competition is no cheating is allowed. The
judges may penalize or disqualify entrants in case of unfair
competition behavior and may adjust the competition rules to prevent
future abuse.
- It is allowed to modify the verification system during the
competition. This is to be noted in the solution(s)
- All techniques used must be general-purpose, and are expected to
extend usefully to new unseen problems
- Internet access is allowed, but using the interget to search for
problem solutions is not.
- Involvement of other people beyond those on the team is not allowed.
- While care is taken to ensure correctness of the reference
implementations supplied with problem descriptions, the organizers
do not guarantee that they are indeed correct.
(We acknowledge Geoff Sutcliffe for inspiring/suggesting some of these
rules.)