http://www.dis.uniroma1.it/~degiacomo/didattica/metodiformali/aa2008-09/
SAPIENZA Università di Roma, Laurea Magistrale in Ingegneria Informatica
Metodi Formali per il Software e i Servizi
Prerequisiti. Si richiede la conoscenza dei fondamenti dell'analisi e progettazione orientata agli oggetti, delle basi di dati relazionali e delle nozioni base della logica del prim'ordine (corsi: Progettazione del Software I, Basi di Dati, Linguaggi e sistemi formali e/o Intelligenza Artificiale).
Obiettivi.
L'obiettivo del corso è lo studio e l'approfondimento della qualità più importante del software: la correttezza. Lo studio della correttezza verrà affrontato con riferimento ad aspetti concettuali e realizzativi affrontando la modellazione e la verifica sia di aspetti statici che di aspetti dinamici. Gli argomenti vengono trattati dando enfasi ad aspetti metodologici e ad aspetti sperimentali utilizzando varie forme di logica (logica del prim'ordine, lodiche descrittive, logiche dinamiche e logiche temporali) e vari strumenti per la verifica automatica. Alla fine del corso lo studente dovrebbe avere acquisito tecniche e metodi per la dimostrazione della correttezza dei programmi e degli schemi concettuali.
Materiale didattico.
[ 1] Slides del corso, A.A. 2008/09. Disponibili in
questa pagina (si veda sotto "materiale didattico").
Informazioni sulla edizione del corso per l'A.A.
2008/09
(Corso erogato nel secondo semestre, dal 2 marzo al 5 giugno 2008)
Avvisi
In questa
sezione vengono riportati gli avvisi specifici sul corso, non sul ricevimento
o altre questioni didattiche, per queste ultime consultare la pagina della didattica.
- Orario ricevimento
studenti: si veda sito didattica del docente.
- Lezioni: aula B2, via Ariosto 25; martedì, ore 14:00-15:30 (2 ore); mercoledì, ore 14:00-17:20 (4 ore).
- Registro delle lezioni
- Materiale didattico
- Programma d'esame
- Modalita' d'esame
- L'esame comprende una prova scritta ed la discussione dello scritto.
- Nota: gli studenti che devono sostenere l'esame nella modalità 5 CFU (eg. Metodi formali nell'ingegneria del software - ordinamento 2000) sosterranno esattamente la stessa prova scritta e la discussione dello scritto di coloro che sostengono l'esame nella modalità 6 CFU (ordinamento corrente), con l'unica differenza che i due argomenti contrassegnati con * nel programma (cioè query epistemiche e OBDD) sono considerati opzionali.
- Appelli
- Primo appello:
prenotazioni dal 04/06/2009
al 09/06/2009. Testo e Risultati.
- DATA: 12 giugno 2009
- ORARIO: 10:45
- AULA: 1, Via Eudossiana 18
- ORALE & VERBALIZZAZIONE: La verbalizzazione avverrà il 22 luglio 2009 alle 16:00 in Via Ariosto 25, aula A3.
- Secondo appello:prenotazioni
dal 12/06/2009 al 29/06/2009 (Per prenotazone esame Metodi formali nell'ingegneria del software - ordinamento 2000, mandare una email al docente). Testo e Risultati.
- DATA: 2 luglio 2009
- ORARIO: 9:30
- AULA: 1, Via Eudossiana 18
- ORALE & VERBALIZZAZIONE: La verbalizzazione avverrà il 22 luglio 2009 alle 17:00 in Via Ariosto 25, aula A3.
- Primo appello di recupero: prenotazioni
dal 02/07/2009 al 06/09/2009.
Testo e Risultati.
- DATA: 9 settembre 2009
- ORARIO: 9:30
- AULA: 1, Via Eudossiana 18
- ORALE & VERBALIZZAZIONE: La verbalizzazione avverrà il 14 ottobre 2009 alle 18:00 in Via Ariosto 25, stanza B215, secondo piano.
- Appello Straordinario: prenotazioni dal 22/10/2009 al 18/11/2009.
Secondo la delibera del Consiglio della Facoltà di Ingegneria dell'Informazione del 21/10/2009 a questo appello possono partecipare SOLO "gli studenti fuori corso, ripetenti, lavoratori e che abbiano terminato la frequenza regolare dei corsi del terzo anno per la laurea e del secondo anno per la laurea specialistica". Pertanto tutti gli studenti che vogliano partecipare questo appello dovranno prenotarsi attraverso il sistema INFOSTUD in modo che possano essere fatti i controlli del caso dalla segreteria, inclusi coloro che intendono sostenere l'esame di Metodi formali nell'Ingegneria del Software - ordinamento 2000 - 5CFU. Testo e Risultati.
- DATA: 20 novembre 2009
- ORARIO: 14:00
- AULA: A3, Via Ariosto 25
- ORALE & VERBALIZZAZIONE: La verbalizzazione avverrà il 3 dicembre 2009 alle 11:00 in Via Ariosto 24, stanza B215, secondo piano.
- Secondo appello di recupero: prenotazioni
dal 21/12/2009 al 24/01/2010.
Testo e Risultati.
- DATA: 27 gennaio 2010
- ORARIO: 9:30
- AULA: 33, Via Eudossiana 18
- ORALE & VERBALIZZAZIONE: La verbalizzazione avverrà l'11 febbraio 2010 alle 15:00 in Via Ariosto 25, stanza B215, secondo piano.
- Terzo appello di recupero: prenotazioni dal 27/01/2010 al 14/02/2010. Testo e Risultati.
- DATA: 16 febbraio 2010
- ORARIO: 14:00
- AULA: 33, Via Eudossiana 18
- ORALE & VERBALIZZAZIONE:La verbalizzazione avverrà il 18 marzo 2010, alle 11:00 nell'ufficio del docente in Via Ariosto 25, secondo piano stanza B215.
- Appello Straordinario: prenotazioni dal 02/04/2010 al 13/04/2010.
Secondo la delibera del Consiglio della Facoltà di Ingegneria dell'Informazione del 21/10/2009 a questo appello è "riservato a: studenti iscritti fuori-corso; studenti iscritti ripetenti, limitatamente agli esami dell'anno che ripetono e degli anni precedenti; studenti lavoratori ufficialmente noti alla segreteria, che abbiano ottenuto il regime di part-time. Il riconoscimento dello status di studenti fuori corso e di quelli che hanno completato la frequenza si effettua sulla base della ricevuta di prenotazione prestampata da INFOSTUD. Per la laurea di base, deve risultare l'immatricolazione nell'a.a. 2006-07 o precedente. Per la laurea specialistica, o magistrale, l'immatricolazione deve essere avvenuta nell'a.a. 2007-08 o precedente. E' causa di esclusione dall'appello straordinario il mancato possesso della ricevuta da parte dello studente. Nei casi di studenti trasferiti, l'anno di immatricolazione potrebbe essere successivo a quelli suddetti. In tale evenienza, la ricevuta dovrà essere accompagnata da un documento idoneo ad attestare che l'immatricolazione in questa Università sia avvenuta a un anno successivo al primo, in modo da permettere di constatare l'avvenuto completamento dell'ultimo anno di corso. Gli studenti ripetenti e part-time da ammettere agli appelli straordinari sono esclusivamente quelli che risultano in tale stato per l'a.a. 2009-10. Gli studenti che non hanno diritto a partecipare all'appello sono vivamente pregati di evitare di prenotarsi, affinché non diventi ancor più complicata l'organizzazione logistica, con danno per gli aventi diritto". Pertanto tutti gli studenti che vogliano partecipare questo appello dovranno prenotarsi attraverso il sistema INFOSTUD in modo che possano essere fatti i controlli del caso dalla segreteria, inclusi coloro che intendono sostenere l'esame di Metodi formali nell'Ingegneria del Software - ordinamento 2000 - 5CFU.
- DATA: 16 aprile 2010
- ORARIO: 15:40
- AULA: 11, Via Scarpa
- ORALE & VERBALIZZAZIONE: da definirsi
Ritorno alla didattica
di Giuseppe De Giacomo