SAPIENZA Università di Roma, Laurea Magistrale in Ingegneria Informatica

Metodi Formali per il Software e i Servizi

Lezioni A.A. 2008/09

docente: Giuseppe De Giacomo


Registro delle lezioni

Settimana Argomento Martedì (ore 14:00:-15:30) Mercoledì (ore 14:00-17:20)
1:02-08mar FOL e Query Congiuntive

Lezioni 1,2
- Introduzione al corso
- Richiami di Logica del Primo Ordine (FOL)



Lezioni 3-6
- Formule aperte e chiuse
- Implicazione logica
- Valutazione di una formula
- Teoria delle query congiuntive


2:09-15mar Formalizzazione dei Diagrammi delle classi UML
Lezioni 7,8
- Il teorema di Chandra-Merlin
- Contenimento tra query congiuntive
- Unioni di query congiuntive (query positive)

Lezioni 9-12
-Richiami su diagrammi delle classi UML
- Formalizzazione dei diagrammi delle classi in FOL

3:16-22mar Formalizzazione dei Diagrammi delle classi UML

Lezione annullata

Lezione annullata

4:23-29mar Formalizzazione dei Diagrammi delle classi UML Lezioni 13-14
- Formalizzazione dei diagrammi delle classi in FOL

Lezioni 15-18
- Le logiche descrittive
- Tableaux per concetti ALC

5:30mar-5apr Formalizzazione dei Diagrammi delle classi UML Lezioni 19-20
- Tableaux per basi di conoscenza ALC
- EXPTIME Hardness del ragionamento su diagrammi UML

Lezioni 21-24
- Uso di logiche descrittive (ALCQI) per ragionare sui diagrammi
- OWL-DL e tool di ragionamento (Ing. Corona)

6:6mar-12apr Formalizzazione dei Diagrammi delle classi UML

Lezioni 25-26
- Ancora su uso di logiche descrittive espressive per ragionare su UML

Vacanze Pasqua

7:13mar-19apr Interrogazioni su Diagrammi delle classi UML
Vacanze Pasqua

Lezioni 27-30
- Query congiuntive su diagrammi UML
- DL-liteA

8:20-26apr

Interrogazioni su Diagrammi delle classi UML

Lezioni 31,32
- Query epistemiche

Lezioni 33-36
- Pre & Post in OCL
-Semantica di valutazione dei programmi
-Semantica di tranzizione dei programmi

9:27apr-03mag Pre/Postcondizioni nei programmi Lezioni 37,38
- Hoare Logic

Lezioni 39,42
- Esercizi: da UML a DLliteA
- Query congiuntive ed epistemiche in DLLitaA per esprimere proprieta sulle classi UML
- Uso del sistema QuOnto per DLliteA

10:04-10mag Model checking Lezioni 43,44
- Introduzione al model checking

Lezioni 45,48
- Transition systems
- Logiche temporali: CTL e LTL, mu-calculus

11:11-17mag Model checking Lezioni 49,50
- Model checking in CTL: valutazione della formula sul transition system

Lezioni 51,54 (Fabio Patrizi)
- Il model checker SMV

12:18-24mag Model checking Lezioni 55,56 (Fabio Patrizi)
- OBDDs

Lezioni 57,58 (Fabio Patrizi)
- OBDDs
- Uso del tool di model checking SMV

13:25-31mag Model checking Lezioni 59,60
- LTL
- Automi di Buchi su stringhe infinite
- Model checking in LTL: manipolazione di automi di Buchi

Lezioni 61,64
- Esercizi d'esame


Home page del corso di Metodi Formali per il Software e i Servizi
della Laurea Magistrale in Ingegneria Informatica, SAPIENZA Università di Roma.