HWMCC'10
Rules
The competition is still in its infancy.
Thus we focus on attracting as many benchmarks and model checkers as possible.
Rules are not applied strictly.
Input and Output Format
The input and output format requirements are described in the AIGER format report.
We are currenlty extending the format to model multiple properties and liveness through generalized Büchi-Automata.
In case you have benchmarks and model checkers for liveness, more specifically, fair loop detection, please contact the organizers.
Another direction is to include word-level model checkers as well.
Execution Environment
- Operating System: Ubuntu Linux
- Processor: Intel Quad Core, 2.6 GHz
- Memory: 8 GB (7 GB memory limit enforced)
- Time: limited to 900 seconds
Assessment of Solvers
Solvers are evaluated based on the number of instances solved and the total time needed.
Prizes
Prized are awarded in three different categories, SAT, UNSAT, and ALL.Restrictions
Due to limited computational resources, the organizers reserved the right not to accept more than 4 different model checkers from the same organization.
The organizers also reserved the right to submit their own systems — or other systems of interest — to the competition.