WELCOME

Hello! I’m a researcher in computer science, focusing on formal and algorithmic aspects of temporal reasoning, including temporal logic and automated planning.

News

April 18, 2025: I’ll be giving a short talk during the special session on MoXI of SPIN 2025, in Hamilton, Canada. See you there!

March 22, 2025: I’ll be giving a tutorial on first-order temporal logic at TIME 2025 in London! See you there!

Research topics

I’m currently focused on formal aspects of automated planning and the verification and reactive synthesis of infinite-state systems specified through first-order temporal logics.

I’m one of the main developers of BLACK, a satisfiability checker supporting both propositional and first-order variants of linear temporal logic.

The following are some interesting recent publication highlights. See all…

Luca Geatti, Alessandro Gianola, Nicola Gigante

First-Order Automata.

AAAI 2025, 14940-14948

Full Text BibTeX

Luca Geatti, Nicola Gigante, Angelo Montanari, Gabriele Venturato

SAT Meets Tableaux for Linear Temporal Logic Satisfiability.

J. Autom. Reason., 68(2), 6

Full Text BibTeX

Michele Chiari, Luca Geatti, Nicola Gigante, Matteo Pradella

SMT-Based Symbolic Model-Checking for Operator Precedence Languages.

CAV (1) 2024, 387-408

Full Text BibTeX

Teaching

I’ve been teaching for a few years the Computer Architecture course at the bachelor degrees in Electronic and Information Engineering and Computer Science at the Free University of Bozen-Bolzano in Italy.

I’ve taught many classes during the years including Mathematical Analysis, C programming (as part of the Operating Sytems course) and Software Security (as part of the CyberChallenge.IT program).