HWMCC Logo

HWMCC'14

CAV Edition

Google Group

Pictures



Vienna Summer of Logic


sponsors:

Oski Technology
ARiSE
Aalto Shool of Science

HWMCC'14

CAV Edition

Affiliated to CAV'14 and FLoC'14 Olympic Games
Vienna, Austria, July 18-22, 2014

Previous Editions

HWMCC'13, HWMCC'12, HWMCC'11, HWMCC'10, HWMCC'08, and HWMCC'07.

This was the 7th competitive event for hardware model checkers.

Winners

Gödel medals were awarded to the best teams of each of the three tracks.

However, every team could only obtain one medal. Tracks are ranked by their importance, deep bound track first, single track second, liveness track last.

Deep Bound Track

  1. TIP by Niklas Sörrenson and Koen Claessen, Chalmers University of Technology, Sweden.
  2. ShiftBMC by Norbert Manthey, Technical University of Dresden, Germany.
  3. NuXMV by Alberto Griggio, Marco Roveri and Alessandro Cimatti, Fondazione Bruno Kessler, Italy.

Gödel medal and $500 check goes to TIP.

Single Safety Property Track

  1. ABC by Baruch Sterin, Robert Brayton, Niklas Eén and Alan Mishchenko, University of Calfornia at Berkeley, USA.
  2. V3 by Cheng-Yin Wu and Chung-Yang (Ric) Huang, National Taiwan University, Taipei, Taiwan.
  3. IIMC by Michael Dooley, Fabio Somenzi, Zyad Hassan and Aaron Bradley, University of Colorado at Boulder, USA.

Gödel medal goes to ABC.

Liveness Track

  1. ABC by Baruch Sterin, Robert Brayton, Niklas Een and Alan Mishchenko, University of Calfornia at Berkeley, USA.
  2. IIMC by Michael Dooley, Fabio Somenzi, Zyad Hassan and Aaron Bradley, University of Colorado at Boulder, USA.
  3. NuXMV by Alberto Griggio, Marco Roveri and Alessandro Cimatti, Fondazione Bruno Kessler, Italy.

Gödel medal goes to IIMC.

Details

The results were presented on the second day of the main part of CAV'14.

Medals and certificates were handed over in the second ceremony of the FLoC'14 Olympic Games on next to last day.

The benchmarks are available as hwmcc14benchmarks.7z.

Beside slides and log files we have:

We are working on making more material available soon.

Setup

Model checkers were required to produce witnesses for single safety properties. These traces were checked by the AIGSIM tool, which is part of the AIGER tools.

Otherwise, the competition was run almost the same way as in the previous two years, except that more powerful hardware was used.

The competition was run on a cluster at Aalto University, with exclusive access to 32 nodes of 2x Six-Core AMD Opteron 2435 2.6GHz with at least 16 GB of RAM. This meant 12 cores for each solver per benchmark, memory limit around 15 GB and time limit of 900 seconds.

Beside the requirement to produces witnesses, rules, input and output format did not change. Please consult the pages of HWMCC'12 for more details. The Oski benchmarks from 2013 which contained uninitialized latches were reencoded to conform to the pre AIGER 1.9 format. All benchmarks only have zero initialized latches.

There were three real silver medals handed out to the winners at the FLoC'14 Olympic Games ceremony in the second week.

Thus it was decided to only have three tracks: the single safety, the liveness and the deep bound track. There was no multiple property track for the CAV edition. It was technically the most challenging one and we only got three medals to hand out.

Organization

HWMCC'14 is organized by Armin Biere, JKU Austria, and Keijo Heljanko, Aalto University Finland.

Sponsors

We are grateful to Oski Technology, which again was sponsoring the deep bound track award.

The winner of the deep bound track got a medal and a check.

The competition was also sponsored by RiSE and Aalto Shool of Science.

Dates

First version of model checkers were due June 1 and updates of model checkers were possible until June 15.