Corso di Metodi Formali

Prof. Silvio Ghilardi -- Dott. Alberto Momigliano

Laurea Magistrale in Informatica - a.a. 2020/2021


AVVISI:

Il corso verrà tenuto in collaborazione col dott. Momigliano ed inizierà Giovedì 1 Ottobre, alle ore 14.30.
Per informazioni, materiale, avvisi si fa riferimento al sito sulla piattaforma Ariel accessibile qui.
Le lezioni si svolgeranno a distanza, utilizzando la piattaforma Microsoft Teams (si consulti il sito Ariel indicato per il codice di accesso).
Di seguito vengono riportate solo le informazioni relative alla parte sul Model Checking gestita dal prof. Ghilardi.


Programma | Orari | Modalità d'esame | Materiali didattici | Appelli d'esame

  1. Programma
  2. La familiarità con lo strumento software costituirà un aspetto particolarmente importante per la preparazione dell'esame: a tale scopo, buona parte delle ore di lezione saranno svolte in laboratorio informatizzato. Per gli studenti interessati (anzichè a NuSMV) al model-checker esplicito SPIN sono in linea qui i lucidi del seminario tenuto dalla Dr. Ing. Paola Spoletini del Politecnico di Milano a conclusione del corso dell'anno accademico 2005-06.

    Bibliografia

    Clarke, Grumberg, Peled, Model Checking, MIT Press, 2000.

  3. Orario delle lezioni.
  4. Si consiglia di controllare regolarmente il sito Ariel del corso per comunicazioni.

    L'orario di ricevimento del prof. Ghilardi è il venerdì mattina alle ore 11.30, presso il Dipartimento di Matematica (via C. Saldini 50).


  5. Modalità d'esame
  6. L'esame per i non frequentanti (per la parte riguardante il Model Checking) sarà costituito da un colloquio e da un progetto.

    Il programma dovrà essere concordato con il docente del corso.

    Sono previsti compitini di esonero totale per i frequentanti.

  7. Materiali didattici
  8. I materiali didattici del corso (dispense, slides, file di esercizi) verranno via via immessi sul sito Ariel del corso.

  9. Appelli d'esame
  10. L'esame per i non frequentanti (per la parte riguardante il Model Checking) è su appuntamento e può essere sostenuto (previo accordo con il docente) durante un qualsiasi orario di ricevimento. Per la registrazione formale occorre, dopo aver sostenuto anche la parte curata dal dott. Momigliano, iscriversi al SIFA con almeno una settimana di anticipo, in corrispondenza delle date degli appelli ufficiali.

    Ultimo aggiornamento: 16/9/2020