Benchmarks

From BWare
Jump to: navigation, search
 
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 TPTP format for mono-sorted first order logic;
+
* [[Media:BWare_PO_v1_FOF.tgz|TPTP FOF format]]: this is the regular TPTP format for mono-sorted first order logic;
* TPTP FOF TFF1 format: this is the TPTP format for first order logic with polymorphic types (à la ML);
+
* [[Media:BWare_PO_v1_TFF1.tgz|TPTP TFF1 format]]: this is the TPTP format for first order logic with polymorphic types (à la ML);
* SMT-LIB v2 format: this is the regular SMT format for many-sorted first order logic;
+
* [[Media:BWare_PO_v1_SMT2.tgz|SMT-LIB v2 format]]: this is the regular SMT format for many-sorted first order logic;
* Alt-Ergo native format: this is the input format of Alt-Ergo.
+
* [[Media:BWare_PO_v1_Alt-Ergo.tgz|Alt-Ergo native format]]: this is the input format of Alt-Ergo.
  
  
For further information regarding this release, please read the documentation file here.<br>
+
For further information regarding this release, please read the documentation file [[Media:readme.pdf|here]].<br>
In particular, before using or integrating this benchmark, carefully read the licensing agreement.
+
Before using this benchmark, carefully read the licensing agreement included in each archive.
 
</div>
 
</div>

Latest revision as of 18:24, 11 March 2015

Personal tools
Namespaces

Variants
Actions
Navigation
Toolbox