Results

Single

The winner of the main single safety / bad-state property track is a new version of suprove by Robert Brayton, Niklas Een, Alan Mishchenko and Baruch Sterin, from Berkeley University, USA.

Live

The winner of the liveness track is tiprbmc by Niklas Sörensson and Koen Claessen from Chalmers University, Gothenburg, Sweden.

Multi

The multi property track was won by the mpmc model checker by Chi-An Wu, Cheng-Yin Wu and Chung-Yang (Ric) Huang from National Taiwan University, Taipei, Taiwan.

Deep Bounds

The deep bounds track award sponsored by Oski Technology was given to tipbmc by Niklas Sörensson and Koen Claessen from Chalmers University, Gothenburg, Sweden.

Niklas Sörensson collecting the award check from Vigyan Singhal.

Details

An overview of the results including full rankings and second and third places can be found in the slides of the presentation from October 24, 2012, at FMCAD'12.

The log files and generated statistics with all the details are available in the following archives:

hwmcc12-live-logs.7z
hwmcc12-multi-logs.7z
hwmcc12-single-logs.7z

Details about the deep bounds track are included in hwmcc12-single-logs.7z, since they are extracted from the single property track log files.

Here are CSV spreadsheets extracted from the analysis of the log files:

single-joined-table.csv
single-flat-table.csv
live-joined-table.csv
live-flat-table.csv

For completeness we included also solvers with discrepancies.

Descriptions

Finally here are more detailed descriptions for the new and rather successful model checkers v3 and mpmc as provided by the authors. In contrast to the other solvers, these did not fit on the slides.