Introduction to formal methods.

Logics for expressing specifications, and static and dynamic properties: first-order logic, temporal logic, fixpoint logics. Logical implication, evaluation of queries, query answering with complete information and incomplete information, conjunctive queries.

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 incomplete databases. Queries over UML class diagrams. Query answering for conjunctive queries (and union of conjunctive queries) under constraints expressed by the UML Class Diagram using the description logics 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,.Fixpoints, 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 mu-calculus. Model checking for CTL via translation to mu-calculus. Model checking for LTL via automata.