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 for automated reasoning on such diagrams. Chase for full dependencies for completing UML Class Diagrams instances.

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. Transition systems based modeling languages for reactive programs: SMV language.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.