Topics for Theses
==============================================
TESI DI LAUREA

- Didattica dell'Informatica
Progettazione e realizzazione di moduli per l'apprendimento interattivo di uno
dei seguenti argomenti:
Logica matematica, Programmazione logica, Programmazione logica con vincoli, Programmazione funzionale, Linguaggi formali e automi

- Verifica di sistemi a stati finiti
Utilizzo di MONA (Weak Monadic Second Order Theory)
Utilizzo di sistemi per il Model Checking
Utilizzo del Concurrency Workbench

- Constraint Logic Programming
Realizzazione di linguaggi CLP che integrino Prolog con vari theorem prover (p.es. ordini discreti, aritmetica di Presburger, numeri reali, ...).
Per tale realizzazione si possono usare tool per l'implementazione di sistemi di vincoli come le Constraint Handling Rules (CHR).
Bibliografia:
A. Yasuhara per l'aritmetica di Presburger;
Thom W. Frühwirth: Theory and Practice of Constraint Handling Rules.
JLP 37(1-3): 95-138 (1998).
http://www.informatik.uni-ulm.de/pm/mitarbeiter/fruehwirth/

- Parsing/Compiling/Pattern-matching
Pattern matching di documenti XML (Articolo di Pierce).

Progetto di un compilatore (C, C++, Java,...) in Prolog
(basato su un articolo di D.H.D. Warren - vedi anche Sterling-Shapiro).

Generazione automatica di un compilatore dalla definizione della sua semantica.

- Specializzazione dell'algoritmo di unificazione

==============================================
TESI DI LAUREA SPECIALISTICA

Vari argomenti nel campo delle metodologie basate sulla logica per la sintesi,
la trasformazione e la verifica dei sistemi software.

- Verifica automatica di proprieta' di sistemi reattivi
  (Model Checking, verifica di sistemi concorrenti e distribuiti,
  verifica di protocolli di sicurezza, verifica di sistemi a stati
  infiniti)
- Sintesi di sistemi reattivi da specifiche formali
- Specializzazione automatica del software
- Automatic derivation of logic programs and constraint logic programs.
- Concurrent and parallel programming.