HWMCC Logo

HWMCC'07

Results
Organizers
Benchmarks
Rules

Rules

Since the last competition in 2007 was the first of its kind and we wanted to attract as many benchmarks and model checkers, the rules were not applied strictly. This will change next year.

Adherence to the input and output format will be required. At most one solver of each group will be allowed in the final run of each category. Splitting the model checkers into a demonstration and competition devision may also be option.

Input and Output Format

The input and output format requirements are described in the AIGER format report. We are actively working on extending the format to model liveness through generalized Büchi-Automata. Another idea is to include word-level model checkers as well.

Execution Environment

  • Operating System: GNU/Debian Linux 2.6.8 (no SMP)
  • Processor: Intel Pentium 4, 3 GHz (hyperthreading switched off)
  • Memory: 2 GB (1.5 GB memory limit for model checking processes enforced)
  • Cache: 1024 KB
  • Compilers: GCC 3.3.5 (might change to 4.0.x), javac 1.5.0_04

Qualification Round

Before the competition there will be a qualification round.

Successful participation is mandatory to qualify.

Assessment of Solvers

Solvers will be evaluated based on the number of instances solved and the total time needed.

Prizes

Prized are awarded in three different categories, SAT, UNSAT, and total.

Restrictions

Due to limited computational resources, the organizers reserve the right not to accept more than 4 different model checkers from the same organization. The organizers also reserve the right to submit their own systems — or other systems of interest — to the competition.