Benchmarks

From BWare
(Difference between revisions)
Jump to: navigation, search
 
(13 intermediate revisions by one user not shown)
Line 2: Line 2:
  
 
<div style="width:690px; float:left;">
 
<div style="width:690px; float:left;">
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 [http://www.cecill.info/licences.en.html 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.
+
 
  
 
In this release, 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
+
* [[Media:BWare_PO_v1_FOF.tgz|TPTP FOF format]]: this is the regular TPTP format for mono-sorted first order logic;
is handled by most of the first order ATPs;
+
* [[Media:BWare_PO_v1_TFF1.tgz|TPTP TFF1 format]]: this is the TPTP format for first order logic with polymorphic types (à la ML);
* TPTP FOF TFF1 format: this is the format for first order logic with polymorphic
+
* [[Media:BWare_PO_v1_SMT2.tgz|SMT-LIB v2 format]]: this is the regular SMT format for many-sorted first order logic;
types (à la ML), which is described in [3];
+
* [[Media:BWare_PO_v1_Alt-Ergo.tgz|Alt-Ergo native format]]: this is the input format of Alt-Ergo.
* 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
+
For further information regarding this release, please read the documentation file [[Media:readme.pdf|here]].<br>
use polymorphic types.
+
Before using this benchmark, carefully read the licensing agreement included in each archive.
 
</div>
 
</div>

Latest revision as of 18:24, 11 March 2015

[edit] 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:


For further information regarding this release, please read the documentation file here.
Before using this benchmark, carefully read the licensing agreement included in each archive.

Personal tools
Namespaces

Variants
Actions
Navigation
Toolbox