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 ;
- 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.