Corso di Metodi Formali (ex Logica II)

Prof. Silvio Ghilardi -- Dott. Alberto Momigliano

Laurea Magistrale in Informatica - a.a. 2016/2017


AVVISI:

Anche nell'anno accademico 2016-2017, il corso verrà tenuto in collaborazione col dott. Momigliano.

Le lezioni del mese di ottobre tenute dal prof. Ghilardi sul model-checking si terranno di giovedì dalle 13 in poi (prima in aula 4 e poi in aula Omega).
Le prime due ore (h.13-14.30) della lezione del 13 ottobre si svolgeranno eccezionalmente nella Sala Riunioni del primo piano
Per la parte di corso gestita dal dott. Momigliano si fa riferimento al sito sulla piattaforma Ariel accessibile qui. 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, lo studente è invitato a installare il sistema NuSMV, a studiarne il tutorial e a preparare qualche file eseguibile (alternativamente, potrà studiare in modo approfondito un esempio significativo incluso nella distribuzione). 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 (per il solo mese di Ottobre).
  4. L'orario di ricevimento del prof. Ghilardi è il venerdì mattina alle ore 11.30, presso il Dipartimento di Matematica (via C. Saldini 50); durante il primo semestre, causa concomitanza con lezioni, l'orario va concordato di volta in volta per email.


  5. Modalità d'esame
  6. L'esame (per la parte riguardante il Model Checking) sarà costitutito da un colloquio. Il programma dovrà essere concordato con il docente del corso.

    Sono previsti compitini per i frequentanti.

  7. Materiali didattici
  8. Due dispense informato elettronico, già in linea qui e qui.

  9. Appelli d'esame
  10. L'esame (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: 10/10/2016