SM/0122/EN - FORMAL METHODS

Academic Year 2019/2020

Free text for the University

Objectives

1. Acquiring knowledge and understanding
The course, devoted to second year students of the Laurea Magistrale in Computer Science, has as main target the achievement of all the knowledges, both theoretical and practical, that will allow the complete comprehension and their effective applicability of the design and verification, using model checking techniques, of a complex system.

2. Applying knowledge and understanding
The course will illustrate methodologies concerning system modeling, and how to formulate and effectively verify
properties the system should enjoy.

3. Making informed judgements and choices
The course provides all the tools and notions to face critically every problem connected to the modeling and
verification of complex systems.


4. Communicating knowledge and understanding
The written proof, with open questions, allows the student to show his capability of exposing in a clear and
coherent manner the treated arguments.

5. Learning capabilities
The course gives an adequate background to be able to face all the problems concerning the design,
development and implementation of programming languages, and gives the key notions to comprehend the
theory and applications of programming languages.

Prerequisites

1. Knowledge
The course does not require any specific knowledge beside the ones acquired in a laurea triennale in Computer Science.

2. Skills
None specific.

3. Competence
None specific.

Preparatory courses:
None.

Contents

The course is organized in 24 lessons concerning both the theory but also the application (each lesson presents an argument in the first part, and in the second part some examples, applications and exercises are provided).

Lessons are divided into three groups:

• 
  in the first group is devoted to the modeling of complex system (transition system), on how to represent the
  computations of a transition system, focussing on concurrency and parallelism, and on how to formalize properties one wish to verify for the system
  


• 
  the lessons the second group focus on the Linear Time Logic (LTL) and on how to do model checking for properties formalized using LTL
  


• 
  in the third group the Computational Time Logic (CTL) is formalized and investigated, in particular on how to do model checking for properties written in CTL, and which are the relations with LTL
  

Teaching Methods

Lectures are given using blackboard. No slides are used, as the book used contains the material illustrated during the lessons, and using the blackboard allows to explain better using the proper pace.

Verification of learning

For each lessons a number of exercise will be proposed, and together with a written exam, will be used in the oral exam.

Texts

Christel Baier & Joost-Pieter Katoen: Principles of Model Checking, MIT Press

More Information

None