Benchmarks

From BWare
(Difference between revisions)
Jump to: navigation, search
Line 4: Line 4:
 
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
 
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.
 
Europe, two industrial partners of the BWare project.
 +
 +
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.
 
</div>
 
</div>

Revision as of 17:53, 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.

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