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

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
InsegnamentiCreditiTAFSSD
12
B
ING-INF/05
12
B
INF/01
12
B
ING-INF/05
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.




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

Codice insegnamento

4S000023

Crediti

6

Lingua di erogazione

Italiano

Settore Scientifico Disciplinare (SSD)

ING-INF/05 - SISTEMI DI ELABORAZIONE DELLE INFORMAZIONI

Periodo

II semestre dal 1 mar 2012 al 15 giu 2012.

Obiettivi formativi

L'insegnamento presenta problemi e metodi per l'analisi e la verifica di programmi, mediante tecniche di ragionamento automatico quali 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

Dimostrazione automatica di teoremi 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 per la soddisfacibilità modulo teorie: uguaglianza, strutture di dati, loro combinazione.

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.
Appelli: 5 (2 a giugno-luglio, 1 a settembre e 2 a febbraio) di cui il I dedicato all'esame mediante prove parziali.
Non è possibile il "rifiuto" del voto: tutti i voti saranno registrati; lo studente può ritirarsi non consegnando.

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