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