| Settimana | Argomento | Mercoledì (ore 10:15:-11:45) | Venerdì (ore 10:15-13:30) |
| 1:26sett-02ott | FOL e Query Congiuntive | Lezioni 1-2 |
Lezioni 3-6 |
| 2:03-09ott | FOL e Query Congiuntive | Lezioni
7-8 | Lezioni 9-12 |
| 3:10-16ott | Formalizzazione dei Diagrammi delle classi UML | Lezioni 13-14 - Contenimento tra query congiuntive - Unioni di query congiuntive (query positive) |
Lezioni 15-18 |
| 4:17-23ott | Interrogazioni su Diagrammi delle classi UML | Lezioni 19-20 - Le logiche descrittive - Tableaux per concetti ALC - Tableaux per basi di conoscenza ALC |
Lezioni 21-24 |
| 5:24-30ott | Interrogazioni su Diagrammi delle classi UML | Lezioni 25-26 Demo del sistema Quonto per ontology based data access (Marco Ruzzi) |
Lezioni 27-30 |
| 6:31ott-06nov | Pre/Postcondizioni nei programmi | Lezioni 31-32 |
Lezioni 33-36 - Pre & Post nei programmi - Transition systems - Semantica di valutazione dei programmi - Semantica di transizione dei programmi |
| 7:07-13nov | Pre/Postcondizioni nei programmi | Lezioni 37-38 - Hoare Logic |
Lezioni 39-42 - Punti fissi - Least and greatest fixpoint - Teorema di Knaster-Tarski - Approssimanti per least-fixpoint - Approssimanti per greatest-fixpoint - Teorema degli approssimanti |
| 8:14-20nov | Teoria dei punti fissi & mu-calculus |
Lezioni 43-44 - Least and greatest fixpoint - Il mu-calculus - Model checking del mu-calculus |
Lezioni 45-48 |
| 9:21-27nov | Model checking | Lezioni 49-50 |
Lezioni 51,54 |
| 10:28nov-04dic | Model checking | Lezioni 55,56 - LTL - Automi di Buchi su stringhe infinite - Model checking in LTL: manipolazione di automi di Buchi |
Lezioni 57,60 |
| 11:05-11dic | Ripasso & Esercizi d'esame | Lezioni 61-62 - Ripasso programma - Esercizi d'esame |
Lezioni annullata |
| 12:12-18dic | Ripasso & Esercizi d'esame | Lezioni 63-64 |
Esame |