Sono disponibili presso il laboratorio di Metodi Formali (Lab. OF/a) tesi di laurea quinquennale o magistrale teoriche e/o implementative su tematiche di ricerca relative 
all'applicazione della teoria dei giochi per la verifica formale di sistemi hardware e software. 
Tutte le tematiche ricadono all'interno di progetti di ricerca internazionali recentemente avviati.

Di seguito alcuni esempi di argomenti di tesi.

1. Teoria dei giochi applicata alla verifica formale di sistemi hardware e software. 
La verifica del corretto funzionamento di un sistema (hardware o software) puo' essere ricondotta alla soluzione di un gioco a due o piu' giocatori, 
su un un opportuno grafo labellato, dove la correttezza del sistema e' espressa in termini di una condizione di vittoria, come ad esempio: 
 - raggiungere un particolare nodo, 
 - percorrere solo percorsi di un determinato tipo, 
 - ciclare all'infinito solo su una parte del grafo
 - oppure, tramite formule espresse tramite una logica opportuna (come le logicche temporali LTL o CTL)
L'obiettivo della tesi e' dunque, dato un particolare gioco, definire, laddove possibile, 
un algoritmo che permetta di calcolare l'esistenza di una strategia vincente per uno dei due giocatori e studiarne la relativa complessita' asintotica.

2. Realizzazione di un tool game-based per la verifica di sistemi software.
Grazie ad algoritmi di model checking, oggi e' possibile verificare in automatico la correttezza di vari tipi di sistemi hardware e software (ma non tutti). 
Tecniche di model checking vengono usate regolarmente dalla Motorola, IBM, INTEL, Miscrosoft, ecc. per testare 
parte dei sistemi da loro prodotti, prima di essere messi in commercio. 
Come ulteriore evidenza dell'importanza del model checking, si ricorda che gli inventori di questa tecnica 
(Edmund M. Clarke, E. Allen Emerson and Joseph Sifakis) sono stati premiati nel 2007 con il Turing Award, il massimo riconoscimento in campo informatico.
L'idea del model checking e' semplice ma efficace: dato un sistema, si considera un suo modello computazionale (per esempio, un grafo di stati labellati), 
si definisce formalmente (tramite una specifica) il suo comportamento desiderato (o malfunzionamenti di cui se ne vuole escludere l'esistenza) 
e poi si verifica se il modello incontra (soddisfa) la specifica o meno.
L'obiettivo della tesi e' quello di creare un tool (oppure estendere tool esistenti) per la verifica di nuove tipologie di software, 
o migliorare la performance di quelli esistenti. 

Al conseguimento della laurea esiste la possibilita' di realizzare un breve periodo di ricerca presso uno dei centri di ricerca esteri coinvolti 
nelle tematiche di tesi, utilizzando una scholarship di progetto.