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.