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.

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/2026

Il 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.

CURRICULUM TIPO:

1° Anno 

InsegnamentiCreditiTAFSSD
12
B
ING-INF/05
12
B
INF/01
12
B
ING-INF/05

2° Anno   Attivato nell'A.A. 2019/2020

InsegnamentiCreditiTAFSSD
6
B
INF/01
Altre attivita' formative
4
F
-
Prova finale
24
E
-
InsegnamentiCreditiTAFSSD
12
B
ING-INF/05
12
B
INF/01
12
B
ING-INF/05
Attivato nell'A.A. 2019/2020
InsegnamentiCreditiTAFSSD
6
B
INF/01
Altre attivita' formative
4
F
-
Prova finale
24
E
-
Insegnamenti Crediti TAF SSD
Tra gli anni: 1°- 2°

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.




S Stage e tirocini presso imprese, enti pubblici o privati, ordini professionali

Codice insegnamento

4S003252

Coordinatore

Andrea Masini

Crediti

6

Lingua di erogazione

Italiano

Settore Scientifico Disciplinare (SSD)

INF/01 - INFORMATICA

Periodo

II semestre dal 4 mar 2019 al 14 giu 2019.

Obiettivi formativi

Il corso si propone di fornire le basi teoriche delle principali tecniche di specifica e verifica di sistemi a stati finiti. In particolare, con riferimento ai sistemi di transizione, tecniche basate sulle tracce, sulla logica del tempo lineare e sulla logica del tempo ramificato.

Al termine del corso lo studente dovrà dimostrare di avere acquisito le conoscenze necessarie per ragionare formalmente su sistemi a stati finiti, con enfasi sui problemi di correttezza risolti in modo automatico (model-checking), attraverso metodi operazionali (tracce) logici (logiche temporali) ed algoritmici.

Queste conoscenze consentiranno allo studente di: i) specificare e provare formalmente proprietà di correttezza di semplici sistemi presentati come sistemi di transizione; ii) utilizzare logiche temporali (lineari e ramificate) per la specifica di proprietà; iii) padroneggiare metodi semantici per le logiche temporali.

Al termine del corso lo studente sarà in grado di: i) confrontare logiche temporali per la verifica automatica e scegliere tra queste le più adeguate a seconda del contesto d'uso; in fase di definizione di un processo di verifica fare le scelte progettuali più appropriate; ii) proseguire gli studi in modo autonomo nell’ambito della verifica formale.

Programma

Verifica dei sistemi:
l’approccio basato sul model checking
Sistemi di modellazione concorrenti:
sistemi di transizione,
parallelismo e comunicazione,
esplosione degli stati
Proprietà del tempo lineare:
safety e invarianti,
liveness,
fairness
Linear Temporal Logic:
sintassi,
semantica,
fairness,
model checking
Computation Tree Logic:
sintassi,
semantica,
espressività di CTL vs LTL,
fairness,
model checking simbolico
CTL *
Equivalenza e astrazione:
bisimulazione,
bisimulazione e equivalenza in CTL *

Testi di riferimento
Autore Titolo Casa editrice Anno ISBN Note
Christel Baier and Joost-Pieter Katoen Principles of Model Checking MIT press 2008

Modalità d'esame

Esame scritto (un'ora e mezzo per svolgere il compito).
Al fine di superare l'esame lo studente deve avere una conoscenza sufficiente di tutti gli argomenti (incluse le prove dei teoremi) e la capacità di risolvere esercizi simili a quelli visti durente le lezioni.
Migliore è la conoscenza degli argomenti del corso, migliore è il risultato dell'esame.

Le/gli studentesse/studenti con disabilità o disturbi specifici di apprendimento (DSA), che intendano richiedere l'adattamento della prova d'esame, devono seguire le indicazioni riportate QUI