Home
Separation Logic
Specs
Tools
Thanks
Competition rules and specifications
- The rules for submitting the solvers and for computing the score for each division are the ones defined for SMT-COMP 2014.
-
The solvers shall run on the StarExec platform.
-
One problem is encoded by one benchmark file. The format of this file is explained
on the wiki of the
GitHub project of the competition
and in the following draft paper.
A problem may be:
- check the satisfiability of a formula A,
- check the validity of an entailment A => B.
-
The possible answers of a solver are: sat, unsat, unknown.
Last modified: Thu Sep 25 18:05:53 CEST 2014