Formal methods

A.Y. 2015/2016
6
Max ECTS
48
Overall hours
Language
Italian
Course syllabus and organization

Unique edition

Responsible
Lesson period
First semester
ATTENDING STUDENTS
Syllabus
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).


Parte B: Software foundations in Coq

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.

The specificity of this course is that is based around the proof assiatant 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. The all course
is formalized and machine-checked: It is intended to be read alongside an interactive session with Coq.

We will tacke the following points:

(1) Recap of basic tools from logic for making and justifying precise claims
about programs (induction, recursion, rewriting)

(2) the use of proof assistants 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 asorting 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.
NON-ATTENDING STUDENTS
Syllabus
please contact the instructors
Lessons: 48 hours