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

Formal Methods

Academic Year 2013/14

Giuseppe De Giacomo


Lecture Diary

-->
Week Topic Wednesday (10:15:-11:45) Thursday (15:45-19:00)
1:Oct 07-13 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 14-20 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 21-27 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
- Complexity of reasoning on UML class diagrams

4:Oct 28-Nov 3 Formalizing UML Class Diagrams

Lectures 19-20
- Incomplete databases
- Certain answers
- CQs in incomplete databases

Lectures 21-24
- CQs over UML class diagrams
- Complete vs incomplete information
- CQs over DLs KBs
- DL-liteA

5:Nov 4-Nov 10 Query Answering through UML Class Diagrams

Lectures 25-26
- DL-liteA
- Query answering in DL-liteA

Lectures 27-30
- Reasoning in DL-liteA

- Semantics of programs
- Structural operational semantics
- Evaluation semantics

6:Nov 11-17 Semantics of programs

Lectures 31-32
- Structural operational semantics
- Transition semantics
- Concurrency

Lectures 33-36
- Hoare Logic

7:Nov 18-24 Fixpoint theory

Lectures 33-34
- Fixpoints
- Least and greatest fixpoints
- Knaster-Tarski theorem
- Approximates of least-fixpoint
- Approximates of greatest-fixpoint
- Approximates theorem

Lectures 35-38
- Least and greatest fixpoints
- Approximates of least-fixpoint
and greatest-fixpoint
- Transition Systems
- Mu-calculus

8:Nov 25-Dec 01 Model checking Lectures 39-40
- Mu-calculus
- Propeties of mu-calculus
- Evaluating mu-calculus formulas over transition systems: model checking

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

9:Dec 02-08

Model checking

Cancelled

Cancelled

10:Dec 09-16 Model checking

Lectures 45-46
- Linear time framework
- Linear time logic (LTL)
- Properties of LTL
- Expressing safeness, liveness and fainess properties in LTL

Lectures 47-50
- Brancing time framework
- Computational Tree Logic (CTL)
- Properties of CTL
- Expressing safeness, liveness and fairness properties in CTL
- Translation of CTL formulas into mu-calculus
- Model checking in CTL via mu-calclulus modelchecking
- LTL, CTL are uncomparable from the point of view of expressiveness
-CTL*

11:Dec 17-22 Question time and exam exercises

Lectures 51-52
- Model checking in the linear time framework
- Transition systems runs as infinite strings
- Buchi Automata on infinite strings
- LTL model checking as nonemptiness of Buchi automata

Lectures 53-56
- Exam exercises


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