Formal methods

A.Y. 2020/2021
6
Max ECTS
48
Overall hours
SSD
INF/01
Language
Italian
Learning objectives
The course will address formal techniques to improve software reliability, in particular w.r.t. the specification and the proof of software properties. The techniques that we will present are symbolic model checking and theorem proving via proof assistants.
Expected learning outcomes
The student will be able to state and prove some simple properties of software using the tools presented in the course
Course syllabus and organization

Single session

Responsible
Lesson period
First semester
Part A
Lectures: synchronous videolectures via Teams, based on slides and notes with a tablet. We shall propose exercises to be done by the student on the spot with the (free) software used in the course that the student will have to install.

Final written exam to be taken in person.

Part B

Lectures: synchronous videolectures via teams. They will be recorded and made available for the duration of the semester

Teaching materials: no change

Exams: short online tests every 3/4 lectures. A final written exam in presence (if possible), paired to a brief presentation/project authored in groups of 2 persons max. Note that this is subject to change given the number of students and the situation with the pandemic
Course 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).


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.
Prerequisites for admission
We require the student to be acquainted with basic knowledge of logic, ideally having taken the graduate course of Logic.
Teaching methods
Lectures and lab sessions (online)
Teaching Resources
web site:

https://amomiglianol2.ariel.ctu.unimi.it/v5/home/Default.aspx

Part1 A:
Lecture notes available on the web page of the course;
- Clarke, Grumberg, Peled, "Model Checking", MIT Press, 2000.
- manuals that can be downloaded from the NuSMV and MCMT sites.

Part B:
A selection from: https://softwarefoundations.cis.upenn.edu/
Assessment methods and Criteria
The exam (on a 1--30 scale) consists of two parts, following the organization of the course. In both cases, the student may develop a project on a topic chosen with the instructor, having shown competence with the software tools on which the course is based on.
INF/01 - INFORMATICS - University credits: 6
Lessons: 48 hours
Educational website(s)