Home     Separation Logic     Specs     Tools     Thanks    

Competition rules and specifications

The set of 678 benchmarks collected has the following properties:

Property	%
Satisfiability	25%
Entailment	75%
Crafted	41%
Random	59%

The problems have been split into five divisions have been used for this competition based on:

• the kind of recursive definitions used in formulas:
  • only acyclic singly linked lists in divisions sll0a_sat and sll0a_entl
  • extended acyclic lists (nested, skip-lists, doubly linked lists) in division FDB_entl
  • general recursive definitions in divisions UDB_Sat and UDB_entl
• the kind of problem solved: satisfiability or entailment

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.

Last modified: Thu Sep 25 18:05:53 CEST 2014