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
2° Anno Attivato nell'A.A. 2023/2024
| Insegnamenti | Crediti | TAF | SSD |
|---|
| Insegnamenti | Crediti | TAF | SSD |
|---|
| Insegnamenti | Crediti | TAF | SSD |
|---|
4 insegnamenti a scelta2 insegnamenti a scelta (A.A. 2022/23: Quantum computing non erogato; A.A. 2023/24: Progettazione ad alte prestazioni in C++ non erogato)3 insegnamenti a scelta (A.A. 2022/23 Quantum computing non erogato)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 automatica di sistemi (2022/2023)
Codice insegnamento
4S003252
Docente
Coordinatore
Crediti
6
Lingua di erogazione
Italiano
Settore Scientifico Disciplinare (SSD)
INF/01 - INFORMATICA
Periodo
Primo semestre dal 3 ott 2022 al 27 gen 2023.
Obiettivi di apprendimento
Il corso si propone di fornire concetti fondamentali di verifica di sistemi sw/hw, per esempio usando metodi formali di verifica deduttiva e modelli che rappresentano il comportamento del sistema in termini di stati e cammini. Al termine del corso le studentesse e gli studenti (1) avranno acquisito le conoscenze tecniche della verifica basata sulla soddisfacibilità di formule, (2) sapranno usarle per modellare il comportamento di specifici sistemi sw/hw, e (3) saranno in grado di proseguire, anche autonomamente, lo studio e la ricerca nell’ambito dei metodi per la verifica formale di sistemi.
Prerequisiti e nozioni di base
Programmazione, algoritmi, logica proposizionale e logica del primo ordine, al livello offerto da insegnamenti di corso di laurea
Programma
Annotazioni ed invarianti. Correttezza parziale e totale. Metodologie per la verifica deduttiva. Cammini elementari. Condizioni di verifica. Procedure di decisione per la soddisfacibilita' (SAT e SMT).
Bibliografia
Modalità didattiche
Lezioni in classe, esercitazioni in classe, progetto individuale di programmazione svolto indipendentemente a casa o in laboratorio universitario.
Modalità di verifica dell'apprendimento
Primo appello: una prova intermedia scritta durante il corso, una prova finale scritta il giorno del primo appello, e un progetto individuale di programmazione sviluppato indipendentemente durante il corso.
Appelli successivi: una prova scritta.
Criteri di valutazione
Correttezza e completezza delle soluzioni; correttezza, usabilita' e qualita' della documentazione del progetto.
Criteri di composizione del voto finale
Primo appello: 25%PI + 25%PF +50%P dove PI e' il voto nella prova intermedia, PF e' il voto nella prova finale e P e' il voto nel progetto.
Appelli successivi: 100%E dove E e' il voto nella prova scritta.
Lingua dell'esame
Italiano
