BLT: Boogie Less Triggers

What is BLT?

• BLT is a tool that takes programs written in the Boogie IVL and outputs first-order logic conjectures in the TPTP syntax, expressing the verification conditions. TPTP (stands for Thousands of Problems for Theorem Provers) is similar to the default Boogie target language, SMTLib, as they are both based on first-order logic and TPTP is considered as a widely accepted language standard for automated theorem provers. The verification conditions generated by BLT utilized some of the recent improvements of TPTP, hence we suggest to use BLT together with the Vampire theorem prover as its backend (more specifically, our implementation is based on the realization of FOOL logic in Vampire). BLT only supports a subset of the Boogie language at the moment, but we are working on the extension of BLT to further support the full language.

• BLT is accepted by 13th International Conference on integrated Formal Methods (iFM 2017) under the title of “Triggerless Happy: Intermediate Verification with a First-Order Prover”.

Try out BLT

• OSX Binary
• Linux x64 Binary

BLT Usage

See the translation in STDOUT:
BLT --file=<yourBoogieFile.bpl>

Or write them into seperate files:
BLT --file=<yourBoogieFile.bpl> --tofile=True

Another option is to enable Tuple encoding:
BLT --file=<yourBoogieFile.bpl> --usetuple=True

[UPDATE] From THF to TFX

As TPTP recently announced official update, we are currently upgrading our syntax accordingly.

Contact

Does BLT suit your interest? Or do you wish to use BLT for other research? Please feel free drop us a mail anytime!