If you base your work on BLACK, please cite (at least some of) the following works.


Luca Geatti, Alessandro Gianola, and Nicola Gigante. Linear Temporal Logic Modulo Theories over Finite Traces. In Proceedings of IJCAI 2022. 2022. Accepted for publication.


Luca Geatti, Nicola Gigante, and Angelo Montanari. A SAT-Based Encoding of the One-Pass and Tree-Shaped Tableau System for LTL. In Proceedings of TABLEAUX 2019, volume 11714 of LNCS, 3–20. 2019. doi:10.1007/978-3-030-29026-9_1.


Luca Geatti, Nicola Gigante, and Angelo Montanari. BLACK: A Fast, Flexible and Reliable LTL Satisfiability Checker. In Dario Della Monica, Gian Luca Pozzato, and Enrico Scala, editors, Proceedings of GandALF 2021, volume 2987 of CEUR Workshop Proceedings, 7–12. 2021. URL:


Luca Geatti, Nicola Gigante, Angelo Montanari, and Gabriele Venturato. Past Matters: Supporting LTL+Past in the BLACK Satisfiability Checker. In Proceedings of TIME 2021, volume 206 of LIPIcs, 8:1–8:17. 2021. doi:10.4230/LIPIcs.TIME.2021.8.