OVERVIEW

The teaching unit provides an introduction to the principles and usage of formal methods to ensure the correctness of software systems.

AIMS AND CONTENT

LEARNING OUTCOMES

The teaching unit offers an introduction to formal, logically grounded, techniques to ensure the correctness of software systems. It intends to provide participants with the ability to (a) master basic concepts and results about type theories, understanding their connection with logic via the proofs-as-programs correspondence, (b) master basic concepts and results about model checking, understanding the notion of model, specification and model-checking algorithm, (c) use advanced type systems to write correct-by-construction programs, (d) use (linear and branching time) temporal logics to specify and verify software systems, (e) critically
evaluate when to apply formal methods and how they complement other techniques.

AIMS AND LEARNING OUTCOMES

Upon completion of the teaching, students will be able to:

- understand and reason about formal models of the syntax, semantics and type systems of core functional languages
- understand the connection between logic and programming languages via the propositions-as-types/proofs-as-programs correspondence
- use a dependently typed functional language as a proof assistant to write formal machine-checked proofs
- write correct-by-construction programs in a dependently typed functional language
- describe the general process of model-checking
- use some models to describe the behavior of a system
- understand the syntax and the semantics of different linear and branching time  temporal logics and use them to write formal specifications 
- run some model-checking algorithms to verify whether a systems satisfies its specification also using some model-checking tools

PREREQUISITES

The teaching unit has no specific prerequisite. Some basic familiarity with the following topics is useful: propositional logic, formal languages (regular expressions and finite automata), (un)decidability of problems, space and time complexity.

TEACHING METHODS

Lectures and practical exercises 

SYLLABUS/CONTENT

Part 1: Type Theory 

- Elements of a programming language: syntax, semantics and type system 
- Lambda-calculus as a core functional language: terms, reduction, confluence and normalization
- Simple types: function, product and sum types
- Progress, Subject Reduction and Type Soundness
- Intuitionistic propositional logic: proof system, BHK interpretation and proposition-as-types/proofs-as-programs correspondence
- Strong Normalization and consistency
- Dependent types: dependent sums and products, identity types
- Inductive types, pattern matching and recursion
- use of Agda as a programming language and as a proof assistant

Part 2: Model Checking
- Transition systems and product of transition systems
- Linear-time properties
- Safety and Liveness
- Buchi Automata
- Verifying regular and omega-regular properties
- Linear temporal logics
- LTL model-checking
- Computational Tree Logic
- CTL model-checking
- Use of PRISM model-checker

RECOMMENDED READING/BIBLIOGRAPHY

- material provided by the instructors 
- J.Y. Girard, Y. Lafont, P. Taylor. Proofs and Types. Cambridge University Press, 1989.
- M.H.B. Sorensen, P. Urzyczyn. Lectures on the Curry-Howard Isomorphism. Elsevier, 2006.
- J.-P. Katoen, C. Baier. Principles of Model-Checking. The MIT Press. 2008.

TEACHERS AND EXAM BOARD

LESSONS

LESSONS START

According to the calendar approved by the Degree Program Board.

Class schedule

The timetable for this course is available here: Portale EasyAcademy

EXAMS

EXAM DESCRIPTION

The exam consists of a written test followed by an oral test. 

ASSESSMENT METHODS

The written test verifies the student's ability to put into practice the concepts seen in class. The oral test verifies the understanding of the concepts and the ability to illustrate them in an appropriate way.