SAPIENZA Università di Roma, Laurea Magistrale in Ingegneria Informatica

Metodi Formali per il Software e i Servizi

Lezioni A.A. 2009/10

docente: Giuseppe De Giacomo


Registro delle lezioni

-->
Settimana Argomento Martedì (ore 16:35:-19:00) Mercoledì (ore 16:35-19:00)
1:01-07mar FOL e Query Congiuntive

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

Lezioni 4-6
- Formule aperte e chiuse
- Implicazione logica
- Valutazione di una formula

2:08-14mar ---
Lezione annullata

Lezione annullata

3:15-21mar FOL e Query Congiuntive

Lezioni 7-9
- Teoria delle query congiuntive
- Il teorema di Chandra-Merlin
- Contenimento tra query congiuntive

Lezioni 10-12
- Unioni di query congiuntive (query positive)
- Richiami su diagrammi delle classi UML
- Formalizzazione dei diagrammi delle classi in FOL

4:22-28mar Formalizzazione dei Diagrammi delle classi UML Lezioni 13-15
- Formalizzazione dei diagrammi delle classi in FOL

Lezioni 16-18
- Le logiche descrittive
- Tableaux per concetti ALC
- Tableaux per basi di conoscenza ALC

5:29mar-4apr Formalizzazione dei Diagrammi delle classi UML
Vacanze Pasqua
Vacanze Pasqua
6:5-11apr Formalizzazione dei Diagrammi delle classi UML
Vacanze Pasqua

Lezioni 19-21
- EXPTIME Hardness del ragionamento su diagrammi UML
- Uso di logiche descrittive (ALCQI/SHIQ) per ragionare sui diagrammi

7:12-18apr Interrogazioni su Diagrammi delle classi UML

Lezioni 22-24
- Query congiuntive su diagrammi UML
- Informazione completa vs informazione incompleta
- Query congiuntive in logiche descrittive

Lezioni 25-28
- DL-liteA
- Ragionare in DL-liteA

8:19-25apr

Pre/Postcondizioni nei programmi

Lezioni 29-31
- Pre & Post nei programmi
- Semantica di valutazione dei programmi
- Semantica di transizione dei programmi

Lezioni 32-34
- Hoare Logic

9:26apr-02mag Teoria dei punti fissi

Lezioni 35-39
- Punti fissi
- Least and greatest fixpoint
- Teorema di Knaster-Tarski

Lezioni 40-42
- Approssimanti per least-fixpoint
- Approssimanti per greatest-fixpoint
- Teorema degli approssimanti

10:03-09mag Model checking Lezioni 43-45
- Introduzione al model checking
- Transition systems
- Logiche temporali: LTL, CTL e CTL*

Lezioni 46-48
- Model checking in CTL: valutazione della formula sul transition system

11:10-16mag ---
Lezione annullata

Lezione annullata

12:17-23mag Model checking

Lezioni 49-51
- Il mu-calculus
- Model checking del mu-calculus

Lezioni 52,54
- LTL
- Automi di Buchi su stringhe infinite
- Model checking in LTL: manipolazione di automi di Buchi

13:24-30mag Model checking Lezioni 55-57
- Ripasso programma
- Esercizi d'esame

Lezioni 58-60
- Ripasso programma
- 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.