Skip to content

BLACK (Bounded Lᴛʟ sAtisfiability ChecKer)

License

Notifications You must be signed in to change notification settings

black-sat/black

Repository files navigation

BLACK Build Status appveyor MIT Latest release codecov

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

Download