Publications

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

[GGG22]

Luca Geatti, Alessandro Gianola, and Nicola Gigante. Linear temporal logic modulo theories over finite traces. In Luc De Raedt, editor, Proceedings of IJCAI 2022, 2641–2647. ijcai.org, 2022. doi:10.24963/IJCAI.2022/366.

[GGGW23]

Luca Geatti, Alessandro Gianola, Nicola Gigante, and Sarah Winkler. Decidable fragments of LTLf modulo theories. In Kobi Gal, Ann Nowé, Grzegorz J. Nalepa, Roy Fairstein, and Roxana Radulescu, editors, Proceedings of ECAI 2023, volume 372 of Frontiers in Artificial Intelligence and Applications, 811–818. IOS Press, 2023. doi:10.3233/FAIA230348.

[GGM19]

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.

[GGM21]

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: http://ceur-ws.org/Vol-2987/paper2.pdf.

[GGMV21]

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.

[GGMV24]

Luca Geatti, Nicola Gigante, Angelo Montanari, and Gabriele Venturato. SAT meets tableaux for linear temporal logic satisfiability. J. Autom. Reason., 68(2):6, 2024. doi:10.1007/S10817-023-09691-1.