Benchmarks

From BWare
(Difference between revisions)
Jump to: navigation, search
Line 5: Line 5:
 
Europe, two industrial partners of the BWare project.
 
Europe, two industrial partners of the BWare project.
  
Several formats are proposed and are divided into several archives. The considered formats are the following:
+
In this release, several formats are proposed and are divided into several archives. The considered formats are the following:
 
* TPTP FOF format: this is the regular format for mono-sorted first order logic that
 
* TPTP FOF format: this is the regular format for mono-sorted first order logic that
 
is handled by most of the first order ATPs;
 
is handled by most of the first order ATPs;

Revision as of 17:54, 11 March 2015

Release v1

This is the release v1 of the B Proof Obligation (PO) benchmark of the BWare project. This release is under the CeCILL-B license, and consists of a set of 12,876 POs, which has been provided by ClearSy and Mitsubishi Electric R&D Centre Europe, two industrial partners of the BWare project.

In this release, several formats are proposed and are divided into several archives. The considered formats are the following:

  • TPTP FOF format: this is the regular format for mono-sorted first order logic that

is handled by most of the first order ATPs;

  • TPTP FOF TFF1 format: this is the format for first order logic with polymorphic

types (à la ML), which is described in [3];

  • SMT-LIB v2 format: this is the regular format for many-sorted first order logic

that is intended to be used by SMT solvers;

  • Alt-Ergo native format: this is the input format of Alt-Ergo that allows the user to

use polymorphic types.

Personal tools
Namespaces

Variants
Actions
Navigation
Toolbox