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

Formal Methods

Course Program (Preliminary Version)

Academic Year 2012/13

Giuseppe De Giacomo

 


Introduction to formal methods.

Logics for expressing specifications, and static and dynamic properties: first-order logic, conjunctive queries, description logics, temporal logic, fixpoint logics.

Analysis and verification of static aspects.

Syntax and semantics of class-based conceptual diagrams such as UML Class Diagrams and Entity Relationship Diagrams. Verification of static properties. Use of first-order logic and description logics for automated reasoning on such diagrams. Queries over UML class diagrams. Specific description logics ALC, ALCQI, SHIQ, DL-LiteA. Automated reasoning in description logics: tableaux procedures for ALC. Query answering for conjunctive queries (and union of conjunctive queries) in description logics: perfect-rewriting in DL-LiteA.

Analysis and verification of dynamic aspects.

Abstract operational semantics for programs: evaluation semantics (whole computation) and transition semantics (single step of the computation). Precondition, postcondition, invariants of programs. Partial and total correctness. Reactive/interactive programs (finite state), transition systems, abstraction. Fixpoint, Knaster-Tarski theorem on least and greatest fixpoint, approximates for least and greatest fixpoint. Verification of dynamic and temporal properties on transition systems: Safeness, Liveness, Fairness, Strong Fairness. Temporal logic for verification : LTL, CTL, CTL*, mu-calculus. Model checking for CTL. Model checking for mu-calculus.


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