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

Formal Methods

Academic Year 2014/15

Giuseppe De Giacomo


Lecture Diary

Week Topic Wednesday (14:00:-15:30) Thursday (15:45-19:00)
1:Oct 01-02 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 8-9 FOL and CQs

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

Cancelled

3:Oct 15-16 FOL and CQs

Lectures 9-10
- Theory of conjunctive queries (CQs)
- NP completeness of CQs evaluation
- Homomorphism
- Chandra-Merlin Theorem on CQ evaluation


Lectures 11-14
- Query containment
- Chandra-Merlin Theorem on CQ query containment
- Execises on CQs and FOL

4:Oct 22-23 Formalizing UML Class Diagrams

Lectures 15-16
- Incomplete databases
- Certain answers
- CQs in incomplete databases
- UML class diagrams
- Fomalization in FOL

Lectures 17-20
- UML class diagrams
- Fomalization in FOL
- Fomalization of classes
- Formalization of Attributes
- Formalization of Associations
- Mutiplicity constraints


5:Oct 29-30 Formalizing UML Class Diagrams

Lectures 21-22
- Automated reasoning on UML class diagrams
- Complexity of reasoning on UML class diagrams

Lectures 23-24
(Lesson starts at 17:15)

- Instantiations of UML class diagrams without ISAs
- Query instantiation of UML class diagram with ISAs
- Instantiations of UML class diagrams with ISAs


6:Nov 5-6 Query Answering through UML Class Diagrams

Lectures 25-26
- Chase and saturation of intantiations
- Query instantiation of UML class diagram with ISAs
- Structural operational semantics

Cancelled

7:Nov 12-13 Semantics of programs

Lectures 27-28
- Structural operational semantics
- Evaluation semantics
- Transition semantics
- Concurrency

Lectures 29-32
- Hoare Logic
- Weakest preconditions
- Invariants
- Variants

8:Nov 19-20 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

9:Nov 26-27

Model checking

Cancelled

Cancelled

10:Dec 03-04 Model checking

Lectures 39-40
- Mu-calculus
- Properties 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*

11:Dec 10-11 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
- Branching 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*

12:Dec 17-18 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.