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:
We will explore mathematical techniques for improving software
reliability, namely for specifying and reasoning about properties of
software and tools for helping validate these properties.


(1) basic tools from logic for making and justifying precise claims
about programs;

(2) the use of proof assistants (hybrid tools that try to automate the
more routine aspects of building proofs while depending on human
guidance for more difficult aspects) to construct rigorous logical
arguments;

(3) the idea of functional programming, both as a method of
programming and as a bridge between programming and logic;

(4) formal techniques for reasoning about the properties of specific
programs (e.g., that a loop terminates on all inputs, or that a
sorting function actually fulfills its specification); and

(5) the use of type systems for establishing well-behavedness
guarantees for all programs in a given programming language (e.g., the
fact that well-typed Java programs cannot be subverted at runtime).


The specificity of this course is that is based around Coq which
provides a rich environment for interactive development of
machine-checked formal reasoning. The kernel of the Coq system is a
simple proof-checker which guarantees that only correct deduction
steps are performed. On top of this kernel, the Coq environment
provides high-level facilities for proof development. All the course
is formalized and machine-checked: It is intended to be read alongside
an interactive session with Coq.