BLACK (short for Bounded Lᴛʟ sAtisfiability ChecKer) is a tool for testing the satisfiability of formulas in Linear Temporal Logic and related logics.
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, LTLf both on infinite and finite models, and LTLf Modulo Theories
- Robust: rock-solid stability with almost 100% test coverage
- Multiplatform: works on Linux, macOS, Windows and FreeBSD
- Easy to use: easy to install binary packages provided for all major platforms
- Embeddable: use BLACK's library API to integrate BLACK's solver into your code
See the Documentation site to learn how to use BLACK.
See the Documentation page for further information on BLACK's installation.
| Ubuntu ≥ 22.04 | Fedora 36 |
|---|---|
sudo apt install ⟨file⟩ |
sudo dnf install ⟨file⟩ |
Install via Homebrew:
$ brew install black-sat/black/black-sat
Download the self-contained ZIP archive.