BLACK

BLACK (short for Bounded Lᴛʟ sAtisfiability ChecKer) is a tool for testing the satisfiability of LTL and LTLf formulas based on the SAT encoding of the tableau method described here. An in depth description of the encoding and the whole algorithm has been published in the proceedings of the TABLEAUX 2019 conference (see the Publications section below).

BLACK is:

• Fast: based on a state-of-the-art SAT-based encoding
• Lightweight: low memory consuption even for large formulas
• Flexible: supports LTL and LTL+Past both on infinite and finite models
• Robust: rock-solid stability with 100% test coverage
• Multiplatform: works on Linux, macOS, Windows and FreeBSD
• Easy to use: easy to install binary packages provided for all platforms
• Embeddable: use BLACK's library API to integrate BLACK's solver into your code

See the Documentation on how to use BLACK. In particular:

1. Downloads and Installation
2. Usage
3. Input Syntax
4. Publications
5. (coming soon...) BLACK C++ Library API