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

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 ≥ 22.04	Fedora 36

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

black-sat / black

readme