Courses

All information related to the courses I currently teach or have taught in the past at the University of Naples Federico II, including contents, schedules, and teaching materials, is available (mostly in Italian) on my official webpage.

Current Theses and Internships

This section presents a selection of proposals for theses and curricular internships that can be adapted to suit both B.Sc. and M.Sc. students (descriptions in Italian; feel free to contact me if you wish to discuss these topics in English).

General Topic 1: Implementation of components of the Hypatia software framework for the verification, analysis, and processing of formal systems developed in the Hypatia language and its evolving dialects

Questo tema è dedicato allo studio, progettazione e implementazione di componenti del framework software Hypatia, sviluppato nel linguaggio funzionale puro Haskell, per la verifica, l'analisi e l'elaborazione di sistemi formali. Ulteriori informazioni sul progetto Hypatia sono disponibili sulla pagina ufficiale HypatiaFSA (attualmente in costruzione) e nel repository ufficiale su GitHub.

  • Proof Certification for Hypatia Documents
    Il progetto riguarda lo studio e lo sviluppo di uno strumento per la certificazione automatica dei documenti Hypatia, volto a garantirne la correttezza formale all'interno del linguaggio stesso.
  • Compilers Between Hypatia Dialects
    L'obiettivo è l'implementazione di compilatori tra diversi dialetti del linguaggio Hypatia, con particolare riferimento a Sifr, Sunya e Zero, che costituiscono il primo livello della relativa gerarchia.
  • Translators from Existing Formal Languages to Hypatia
    Il lavoro consiste nella progettazione e implementazione di traduttori da linguaggi formali consolidati, come Automath, Metamath, Mizar, Nuprl, Rocq, Matita, Isabelle e Lean, verso Hypatia.
  • Language Server and IDE Integration for Hypatia
    L'attività riguarda la realizzazione di un Language Server Protocol (LSP) per Hypatia, con l'obiettivo di fornire supporto avanzato in ambienti di sviluppo integrati (IDE), come VSCode, Emacs o Vim/NeoVim, gestendo la sintassi, il completamento automatico, la verifica in tempo reale e altre funzionalità interattive per facilitare la scrittura e l'analisi di sistemi formali in Hypatia.

The references listed below provide useful background for the theoretical and methodological framing of the thesis topics.

  • Existing Systems - A collection of established formal systems and proof assistants.
    • Automath – An early system for formalizing and automatically checking mathematical proofs.
      • Manual - A Nice and Accurate Checker for the Mathematical Language Automath, by F. Wiedijk, 1999.
    • Isabelle – A generic proof assistant and logical framework for formal verification.
    • Lean – A modern proof assistant and formal language for mathematics and software verification.
    • Matita – A proof assistant for constructive mathematics and theorem checking.
      • Manual - Matita V0.99.3 User Manual, by the HELM Team, 2006.
    • Metamath – A minimal formal system for strict automated verification of mathematical proofs.
      • Manual - Metamath - A Computer Language for Mathematical Proofs, by N.D. Megill, 2019.
    • Mizar – A readable formal environment for writing and verifying mathematical theorems.
      • Manual - Mizar in a Nutshell, by A. Grabowski, A. Kornilowicz, And A. Naumowicz, 2010.
      • Lecture Notes - Mizar Lecture Notes, by Y. Nakamura, T. Watanabe, Y. Tanaka, and P. Kawamoto, 2002.
      • Early Reference - An Outline of PC Mizar, by M. Muzalewski, 1993.
      • Introductory Guide - An Introduction to PC Mizar, by E. Bonarska, 1990.
    • Nuprl – A proof assistant based on constructive type theory with program extraction.
      • Manual - The Nuprl Proof Development System, by C. Kreitz, 2002.
      • Guide - Implementing Mathematics with The Nuprl Proof Development System, by R.L. Constable et al., 1985.
      • Tutorial - A User-Level Introduction to the Nuprl Proof Development System, by E. Aaron, 2001.
    • Rocq – An interactive proof assistant for formal reasoning based on dependent type theory.
      • Manual - The Rocq Reference Manual, by Inria and CNRS, 2025.

General Topic 2: Implementation and Experimental Evaluation of Decision Procedures for Decidable Fragments of First-Order Logic

Questo tema è dedicato allo studio, realizzazione e valutazione sperimentale di procedure di decisione automatiche per frammenti noti della logica del primo ordine. L'attenzione è rivolta in particolare a tecniche basate sulla risoluzione e alla loro integrazione in sistemi di dimostrazione automatica esistenti, con l'obiettivo di analizzarne efficienza e ambiti di applicabilità.

  • Resolution-Based Decision Procedures for Decidable Fragments of First-Order Logic (FO2, UN, GN, etc.)
    Il tema riguarda lo studio dei principali frammenti decidibili della logica del primo ordine, quali, ad esempio, la logica a due variabili (FO2), il frammento a negazione unaria (Unary Negation, UN) e il frammento a negazione vincolata (Guarded Negation, GN), e l'implementazione di procedure di decisione basate su tecniche di risoluzione. Il progetto può includere l'adattamento di approcci noti, la loro integrazione in un dimostratore automatico e una valutazione comparativa su classi rappresentative di istanze.
  • Decision Procedures for Modal and Temporal Logics via Encodings into First-Order Logic
    L'obiettivo dell'attività è l'esplorazione dell'impiego di traduzioni in logica del primo ordine per il trattamento automatico di logiche modali e temporali mediante dimostratori esistenti. Un possibile caso di studio è la logica 3ML (A Modal Logic for RDF Data), recentemente sviluppata dal docente in collaborazione con colleghi. Il lavoro può comprendere la formalizzazione della traduzione, la sua implementazione automatica e un'analisi critica dei vantaggi e dei limiti dell'approccio.
  • Automatic Generation of Formulae for Decidable Fragments of First-Order Logic
    L'attività prevede la progettazione e l'implementazione di generatori casuali parametrizzati di formule appartenenti a frammenti decidibili. Questi strumenti sono essenziali per la costruzione di benchmark e per la valutazione sperimentale delle procedure di decisione. Il progetto può includere la definizione di modelli probabilistici di generazione, il controllo delle proprietà sintattiche delle formule prodotte e l'impiego sistematico dei generatori in campagne di test.
  • Framework for the Automatic Selection of Decision Procedures in the Vampire Prover
    Questa tema riguarda la progettazione e lo sviluppo di un'infrastruttura modulare integrata nel dimostratore automatico Vampire, in grado di riconoscere automaticamente frammenti decidibili di formule del primo ordine e di selezionare dinamicamente procedure di decisione specializzate. Il progetto può comprendere l'analisi sintattica dei frammenti, l'interazione con il motore di risoluzione e una valutazione sperimentale dell'impatto sulle prestazioni complessive del sistema.

The thesis works developed within this research topic are listed below.

  1. Implementazione di una Procedura di Decisione per il Frammento Guarded in Vampire (in Italian)
    Bachelor thesis by Francesco Scarfato, 2024.
  2. Implementazione di una Procedura di Decisione per Frammenti Binding in Vampire (in Italian)
    Bachelor thesis by Matteo Richard Gaudino, 2024.
  3. Implementation of a Decision Procedure for the Fluted Fragment in Vampire
    Bachelor thesis by Riccardo Elena, 2025.

The references listed below provide useful background for the theoretical and methodological framing of the thesis topics.

Past Theses and Internships

This section lists proposals of theses and curricular internships that were offered in the past.

General Topic: Efficient Solution Algorithms for Infinite-Duration Games on Graphs

This topic was devoted to the study and development of efficient algorithms for solving infinite-duration games on graphs, with particular focus on parity and mean-payoff games. Such models play a central role in formal verification and in the automatic synthesis of hardware and software systems. The research activity focused on analysing the performance of existing algorithms, identifying corner cases that highlight their computational difficulties, and designing new solution techniques aimed at improving scalability and practical effectiveness, supported by thorough experimental evaluations.

The thesis works developed within this research topic are listed below.

  1. Solving Parity Games using Priority Promotion Techniques
    Master thesis by Daniele Dell'Erba, 2015.
  2. Algoritmi Simbolici per la Generazione e Risoluzione di Giochi di Parità. (in Italian)
    Master thesis by Orlando Aprea, 2018.
  3. Solving Infinite Games on Graphs via Quasi Dominions
    Ph.D. thesis by Daniele Dell'Erba, 2019.
  4. Tecniche Di Generazione Di Benchmark Per La Valutazione Empirica Dell'Efficienza Degli Algoritmi Di Risoluzione Di Giochi Su Grafi (in Italian)
    Bachelor thesis by Giuseppe Amato, 2022.

The following publications were developed during this research activity.

  1. Solving Parity Games via Priority Promotion
    M. Benerecetti, D. Dell'Erba, and F. Mogavero at CAV, 2016.
  2. A Delayed Promotion Policy for Parity Games
    M. Benerecetti, D. Dell'Erba, and F. Mogavero at GANDALF, 2016.
  3. Improving Priority Promotion for Parity Games
    M. Benerecetti, D. Dell'Erba, and F. Mogavero at HVC, 2016.
  4. The Priority Promotion Approach to Parity Games
    M. Benerecetti, D. Dell'Erba, and F. Mogavero at ICTCS, 2017.
  5. Robust Exponential Worst Cases for Divide-et-Impera Algorithms for Parity Games
    M. Benerecetti, D. Dell'Erba, and F. Mogavero at GANDALF, 2017.
  6. Solving Parity Games via Priority Promotion
    M. Benerecetti, D. Dell'Erba, and F. Mogavero on FMSD, 2018.
  7. A Delayed Promotion Policy for Parity Games
    M. Benerecetti, D. Dell'Erba, and F. Mogavero on I&C, 2018.
  8. Solving Mean-Payoff Games via Quasi Dominions
    M. Benerecetti, D. Dell'Erba, and F. Mogavero at TACAS, 2020.
  9. Robust Worst Cases for Parity Games Algorithms
    M. Benerecetti, D. Dell'Erba, and F. Mogavero on I&C, 2020.
  10. From Quasi-Dominions to Progress Measures
    M. Benerecetti, D. Dell'Erba, M. Faella, and F. Mogavero in Lecture Notes Series of IMS NUS, 2023.
  11. Solving Mean-Payoff Games via Quasi Dominions
    M. Benerecetti, D. Dell'Erba, and F. Mogavero on I&C, 2024.
  12. Priority Promotion with Parysian Flair
    M. Benerecetti, D. Dell'Erba, F. Mogavero, S. Schewe, and D. Wojtczak on JCSS, 2025.