Studiare
In questa sezione è possibile reperire le informazioni riguardanti l'organizzazione pratica del corso, lo svolgimento delle attività didattiche, le opportunità formative e i contatti utili durante tutto il percorso di studi, fino al conseguimento del titolo finale.
Piano Didattico
Queste informazioni sono destinate esclusivamente agli studenti e alle studentesse già iscritti a questo corso.Se sei un nuovo studente interessato all'immatricolazione, trovi le informazioni sul percorso di studi alla pagina del corso:
Laurea magistrale in Ingegneria e scienze informatiche - Immatricolazione dal 2025/2026Il piano didattico è l'elenco degli insegnamenti e delle altre attività formative che devono essere sostenute nel corso della propria carriera universitaria.
Selezionare il piano didattico in base all'anno accademico di iscrizione.
1° Anno
| Insegnamenti | Crediti | TAF | SSD |
|---|
2° Anno Attivato nell'A.A. 2010/2011
| Insegnamenti | Crediti | TAF | SSD |
|---|
Tre insegnamenti a scelta tra i seguenti | Insegnamenti | Crediti | TAF | SSD |
|---|
| Insegnamenti | Crediti | TAF | SSD |
|---|
Tre insegnamenti a scelta tra i seguenti | Insegnamenti | Crediti | TAF | SSD |
|---|
Legenda | Tipo Attività Formativa (TAF)
TAF (Tipologia Attività Formativa) Tutti gli insegnamenti e le attività sono classificate in diversi tipi di attività formativa, indicati da una lettera.
Verifica (2009/2010)
Codice insegnamento
4S02800
Docente
Coordinatore
Crediti
6
Lingua di erogazione
Inglese
Settore Scientifico Disciplinare (SSD)
ING-INF/05 - SISTEMI DI ELABORAZIONE DELLE INFORMAZIONI
Periodo
II semestre dal 1 mar 2010 al 15 giu 2010.
Obiettivi formativi
L'insegnamento presenta problemi e metodi per l'analisi e la verifica di programmi, mediante dimostrazione automatica di teoremi o model checking. Obbiettivo del corso è che lo studente, oltre a padroneggiare tecniche specifiche, comprenda i problemi inerenti da un lato a esprimere il comportamento dei programmi in formule logiche e dall'altro a progettare ragionatori automatici capaci di gestire tali formule in modo efficiente.
Programma
Teorie al primo ordine. Induzione. Logica di Hoare, annotazioni, correttezza parziale e totale, stati, cammini, invarianti. Generazione di invarianti. Tecniche di ragionamento automatico a scelta tra: procedure di decisione per la soddisfacibilità modulo teorie (uguaglianza, strutture di dati, combinazione di teorie, procedure di decisione basate su risoluzione e sovrapposizione); model checking (model checking simbolico, astrazione su predicati, raffinamento guidato da contro-esempi).
| Autore | Titolo | Casa editrice | Anno | ISBN | Note |
|---|---|---|---|---|---|
| Aaron R. Bradley, Zohar Manna | The Calculus of Computation - Decision Procedures with Applications to Verification (Edizione 1) | Springer | 2007 | 9783540741 | Testo adottato |
Modalità d'esame
Per gli studenti di CdLM/LS:
Esame mediante prove parziali: consta di un compito scritto (C) e di un progetto individuale (P) da realizzare a casa o in laboratorio durante il corso. Il voto d'esame è dato da: 50% C + 50% P. Questa modalità vale solo per il primo appello dopo la fine del corso.
Esame senza prove parziali: consta di un unico compito scritto (E), di difficoltà tale da uguagliare C+P, il cui voto determina il voto d'esame. Questa modalità vale per tutti gli appelli.
Per gli studenti di DdR:
esame orale consistente nella presentazione di uno o più articoli dalla letteratura.
