· Motivations: model checking is a completely automatized tool for the verification of reactive and concurrent systems. · Temporal logics LTL and CTL: syntax and semantics, expressivity comparison, axiomatizations (brief outline), negation normal forms. · Model-checking: examples from network and operating systems topics (mutual exclusion, producer/consumer, dining philosophers, etc.). · Automata on infinite words: Buechi automata, omega-regular languages, emptiness tests and Boolean closure. · Satisfiability and explicit model-checking in LTL: Hintikka sets, formulae as automata, tableaux for LTL. · Fixpoints of monotone operators: Knaster-Tarski theorem, applications to CTL operators. · Symbolic model-checking in CTL: finite state machines, OBDD (`ordered binary decision diagrams'), symbolic simulation of fixpoint approximations. · Bounded model-checking: SAT reductions and SAT-solver employment in model-checking. · Infinite state model-checking: well-structured systems and backward reachability; the approximate model technique and the stopping failures model; · Infinite state model-checking: recent development of a declarative approach based on SMT-solvers; array-based systems; examples from mutual exclusion protocols, cache coherence protocols, lossy channel systems, fault-tolerant systems, parameterized timed automata. · Software support: introduction to the tools NuSMV (for finite state systems) and MCMT (for infinite state systems).
Part B: The second part of the Formal Methods course consists in a monographic mini-course on logic programming in PROLOG. The mathematical logic fundamentals are introduced together with the theoretical concepts needed for logic programming. Teaching of the logic-programming language PROLOG is supplemented with lab class exercises where PROLOG is used to write programs for problem solving.