Formal Methods

Part A: Model Checking and Temporal Logics

· 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.