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

I’ve joined the Editorial Board of the ETAPS Blog! Thanks to Marieke Huisman and the other members for welcoming me in!
Together with Andrea Micheli, Matteo Cardellini and Gregor Behnke, I’ll be quite busy at ICAPS 2025: we’ll give a tutorial on SAT- and SMT-based techniques for automated planning and will chair a workshop on the same topic. See you in Melbourne!
I’ll be giving a short talk during the special session on MoXI of SPIN 2025, in Hamilton, Canada. See you there!
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 many 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).