BLACK

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
• Flexible: supports LTL and LTL+Past, LTLf both on infinite and finite traces, and LTLf Modulo Theories
• Robust: stability and correct results via extensive testing
• Multiplatform: works on Linux, macOS and Windows
• Easy to use: easy to install binary packages provided for all major platforms

How to use BLACK

See the Documentation site to learn how to use BLACK.

Downloads

See the Documentation page for further information on BLACK’s installation.

Linux

Ubuntu ≥ 24.04	Fedora 41
sudo apt install ⟨file⟩	sudo dnf install ⟨file⟩

macOS

Install via Homebrew:

$ brew install black-sat/black/black-sat

Windows

Download the self-contained ZIP archive.