Last year, the conference VSTTE 2010 organized a competition of software verification systems (language + tools), to improve understanding of each system’s pros and cons. Rod Chapman from Altran Praxis participated with the SPARK language and toolset, and solved the first problem even beyond what the subject asked. We have since provided solutions in SPARK to all five problems, like other teams, which formed the basis for a report that you can find on this page.
This report was deemed important enough by the organizers of the Formal Methods conference 2011 that they have granted it the best paper award.
Furthermore, the page of the competition contains an archive with all solutions in many different languages and systems… you can even DIY!
One Trackback
[...] Best Paper Award for Results of Verification Competition Last year, the conference VSTTE 2010 organized a competition of software verification systems (language + tools), to improve understanding of each system’s pros and cons. Source: http://www.open-do.org [...]