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. 2014/2015
| Insegnamenti | Crediti | TAF | SSD |
|---|
| Insegnamenti | Crediti | TAF | SSD |
|---|
| Insegnamenti | Crediti | TAF | SSD |
|---|
| Insegnamenti | Crediti | TAF | SSD |
|---|
Tre insegnamenti a scelta tra i seguentiLegenda | 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 programmi (2013/2014)
Codice insegnamento
4S000023
Docente
Coordinatore
Crediti
6
Lingua di erogazione
Italiano
Settore Scientifico Disciplinare (SSD)
ING-INF/05 - SISTEMI DI ELABORAZIONE DELLE INFORMAZIONI
Periodo
II semestre dal 3 mar 2014 al 13 giu 2014.
Sede
VERONA
Obiettivi formativi
L'insegnamento presenta problemi e metodi per l'analisi e la verifica di programmi, mediante tecniche di ragionamento automatico. 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 o solutori automatici capaci di gestire tali formule in modo efficiente.
Programma
Procedure di prova in logica proposizionale e al primo ordine. Teorie al primo ordine. Logica di Hoare, annotazioni, correttezza parziale e totale, stati, cammini, invarianti. Generazione e prova di condizioni di verifica per la correttezza parziale e totale. Procedure di decisione: eliminazione di quantificatori, chiusura di congruenza, liste, array, combinazione di procedure per condivisione di uguaglianze.
| Autore | Titolo | Casa editrice | Anno | ISBN | Note |
|---|---|---|---|---|---|
| Daniel Kroening, Ofer Strichman | Decision Procedures. An algorithmic point of view | Springer | 2008 | 978-3-540-74104-6 | |
| Aaron R. Bradley, Zohar Manna | The Calculus of Computation - Decision Procedures with Applications to Verification (Edizione 1) | Springer | 2007 | 9783540741 |
Modalità d'esame
Esame mediante prove parziali:
Il voto è dato da 30% C1 + 35% C2 + 35% P, dove C1 è un compito scritto in classe (prova intermedia), C2 è un compito scritto (prova finale) in programma per il giorno del I appello della sessione estiva, e P è un progetto individuale. Il voto così generato viene registrato al I appello della sessione estiva.
Esame senza prove parziali:
Il voto è dato da 100% E, dove E è un unico compito scritto, di difficoltà tale da uguagliare l'unione delle prove parziali.
Non è possibile il "rifiuto" del voto: tutti i voti saranno registrati; lo studente può ritirarsi informando la docente. Tutti gli elaborati sono individuali; è vietato copiare o condividere codice o testo. Eventuali copiature determinano abbassamenti di voti per tutti gli studenti coinvolti.
