SAPIENZA Università di Roma, MSc in Engineering in Computer Science
(Laurea Magistrale in Ingegneria Informatica)

Formal Methods

Academic Year 2012/13

Giuseppe De Giacomo

Lecture Diary

Week Topic Wednesday (10:15:-11:45) Thursday (15:45-19:00)
1:Oct 01-07 FOL and CQs

Lectures 1-2
- Introduction to the course
- First-order logic

Lectures 3-6
- Open and closed formulas
- Logical implication
- Evaluation of a formula

2:Oct 08-14 FOL and CQs

Lectures 7-8
- Time cost of evaluation
- Space cost of evaluation
- Combined complexity, Data complexity, Query complexity

Lectures 9-12
- Theory of conjunctive queries (CQs)
- NP completeness of CQs evaluation
- Homomorphism
- Chandra-Merlin Theorem
3:Oct 15-21 FOL and CQs Lectures cancelled

Lectures cancelled

4:Oct 22-28 Formalizing UML Class Diagrams Lectures 13-14
- UML class diagrams
- Fomalization in FOL

Lectures 15-18
- Fomalization in FOL
- Automated reasoning on UML class diagrams
- Description logics


5:Oct 29-Nov 04 Formalizing UML Class Diagrams Lectures 19-20
- Description Logics
- Concept satisfiability for ALC
- KB logical implication in ALC

Vacation
6:Nov 05-11 Formalizing UML Class Diagrams

Lectures 21-22

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

Lectures 23-26
- CQs over UML class diagrams
- Complete vs incomplete information
- CQs over DLs KBs
- DL-liteA
7:Nov 12-18 Pre/Postconditions in programs

Lectures 27-28
- DL-liteA
- Reasoning in DL-liteA

Lectures 29-32
- Pre & Post conditions in programs
- Transition systems
- Evaluation semantics of programs
- Transition semantics of programs
8:Nov 19-25 Pre/Postconditions in programs Lectures 33-34
- Hoare Logic 		Lectures 35-38
- Fixpoints
- Least and greatest fixpoint
- Knaster-Tarski theorem
- Approximates of least-fixpoint
- Approximates of greatest-fixpoint
- Approximates theorem
9:Nov 26 - Dec 02

Fixpoint theory & mu-calculus

Lectures 39-40
- Least and greatest fixpoint
- Mu-calculus
- Model checking of mu-calculus: evaluating CTL formulas over transition systems

Lectures 41-44
- Introduction to model checking
- Transition systems
- Temporal logics: LTL, CTL e CTL*

10:Dec 03-09 Model checking

Lectures 45-46
- Model checking in CTL: evaluating CTL formulas over transition systems

Lectures 47-50
- Model checking in CTL
- Relationship with model checking in mu-calculus

11:Dec 10-17 Model checking Lectures 51-52
- LTL
- Buchi Automata on infinite strings
- Model checking in LTL: Buchi automata manipulation

Lectures 53-56
- Safety & liveness in linear time framework
- Verification on finite strings
- Finite state automata for verification
12:Dec 18-23 Ripasso & Esercizi d'esame
Lectures 57-58
- Exam exercises

Pre-exam
(during lecturing hours)

Home of Formal Methods
MSc Engineering in Computer Science, SAPIENZA Università di Roma.