Laboratori & Tesi

In questa pagina descrivo alcuni argomenti di mio interesse, su cui è possibile svolgere dei laboratori avanzati o tesi di laurea (triennale o magistrale). Se qualche argomento è di vostro interesse, possiamo fissare un appuntamento per discutere un progetto preciso (la cui disponibilità varia nel tempo).

Regole generali:

  1. I progetti vengono assegnati su base “first-come first-served, con time-out”: quando un progetto viene assegnato, si fissa anche una data di consegna (tipicamente dai 2 ai 4 mesi, in proporzione alla difficoltà del progetto); se tale data non è rispettata, l’assegnazione decade e il progetto può essere assegnato ad altri studenti.
  2. In generale, tutti i progetti di laboratorio avanzato possono “evolvere” in una tesi di laurea (triennale o magistrale). Tuttavia l’impegno necessario (e di conseguenza il valore in termini di punteggio) di tali tesi è assai variabile. Pertanto il tipo di progetto che viene assegnato dipende anche dall’eventuale evoluzione dello stesso in una tesi di laurea.
  3. I laboratori avanzati comprendono sempre una rilevante parte di programmazione, anche se non necessariamente in linguaggi tradizionali. Questo vincolo non vale per le tesi di laurea, che, in assenza di parte pratica, possono essere “puramente teoriche” o “compilative”.
  4. Tutti i progetti devono essere corredati da una relazione scritta.
  5. In generale, il codice sviluppato viene reso disponibile sotto una licenza open source su questo sito (vedi elenco a lato), per permettere eventuali sviluppi, miglioramenti ed applicazioni ad altre persone interessate.

Potete farvi un’idea degli argomenti anche dall’elenco dei progetti, e dall’elenco delle ultime tesi di cui sono stato relatore, che è reperibile online, impostando “miculan” nel campo “relatore”.

4 thoughts on “Laboratori & Tesi

  1. Modelli grafici di sistemi distribuiti e mobili

    Recentemente, il nostro gruppo di ricerca sta studiando formalismi grafici per rappresentare sistemi distribuiti e mobili (come p.e., reti di calcolatori, processi, thread, etc). In sintesi, lo stato di un sistema mobile-concorrente può essere descritto come una particolare struttura grafica dove vengono rappresentate contemporaneamente la struttura della rete e le connessioni tra i vari nodi. Tale stato evolve secondo un insieme di regole di riscrittura grafiche.

    Il nostro gruppo di ricerca ha avviato una implementazione di questo formalismo grafico; sono già state realizzate le strutture dati base, con alcune operazioni fondamentali, una editor basato su Eclipse. Su questa base ci sono molti possibili sviluppi per laboratori avanzati: implementare una interfacce grafiche “mouse-oriented”, implementare funzionalità per ora descritte solo sulla carta, sviluppare specifiche applicazioni, testing…

    È richiesta una certa attitudine alla programmazione, Java o funzionale (ma non necessariamente).

  2. Logiche di Hoare per thread concorrenti in Isabelle

    Recentemente è stata introdotta una nuova famiglia di Logiche di Hoare per la verifica di programmi paralleli, più agevoli e flessibili dei metodi di Owiki-Gries, e alternativi al rely-guarantee. In particolare abbiamo sviluppato un modello semantico, e la sua logica di Hoare, corrispondente ai thread dinamici con eccezioni, conforme al modello Posix implementato in linguaggi comuni come C, Java, etc.

    In questo progetto si propone di continuare la ricerca in questa direzione, ad esempio lavorando sull’implementazione della logica di Hoare nel proof assistant Isabelle/HOL, o sviluppando semplici esempi di applicazione di tale logica.

    È preferibile aver seguito il corso di Metodi Formali per l’Informatica 1, e conoscere le basi di Logica.

  3. Formalizzazione di protocolli e sistemi concorrenti

    Protocolli e sistemi concorrenti possono essere formalizzati anche usando formalismi “logici”, come ad esempio IsabelleCoq, e il recente CELF.
    In particolare, si vuole studiare l’applicazione di quest’ultimo formalismo a protocolli di sicurezza, allo scopo di verificare formalmente proprietà di sicurezza di tali protocolli.
    È consigliabile una certa attitudine alla programmazione, possibilmente logico-funzionale, e qualche rudimento di logica.

  4. Verifica automatica di protocolli di sicurezza

    In anni recenti sono stati sviluppati diversi tool per la verifica automatica di proprietà di protocolli di sicurezza. Due esempi molto interessanti sono AVISPA e ProVerif.

    Si propone di utilizzare questi strumenti per la verifica di proprietà di qualche protocollo; questo consiste nel rappresentare un protocollo nel formalismo proprio di uno di questi tool, e di impiegare il tool per la verifica delle proprietà rilevanti. Ad esempio, in un recente laboratorio abbiamo formalizzato il protocollo di single-sign in di Google, verificando l’esistenza del bug recentemente scoperto.

    È consigliata una minima conoscenza dei linguaggi logici.

Comments are closed.