Syllabus del corso
Obiettivi
Acquisire la capacità di specificare, modellare e analizzare formalmente sistemi concorrenti; acquisire la capacità di esprimere in linguaggi logici proprietà dei sistemi concorrenti.
Contenuti sintetici
Strumenti teorici per comprendere e manipolare concetti di base dell'informatica relativi al comportamento e alla descrizione di processi distribuiti e concorrenti. Nozioni fondamentali per la verifica di proprietà di programmi e di modelli di sistemi. Uso di logiche formali per specificare proprietà di sistemi.
Programma esteso
- Metodi per la specifica e la verifica di correttezza dei programmi. La
semantica assiomatica dei programmi sequenziali, la logica di Hoare; dimostrazioni di correttezza di programmi sequenziali. - Modelli della concorrenza: modelli di sistemi reattivi, calcoli di
processi (CCS, Calculus of Communicating Systems) e reti di Petri. Nozioni tipiche dei sistemi concorrenti: dipendenza e indipendenza causale, conflitto, confusione, sincronizzazione. - Semantica interleaving (sistemi di transizioni) e a ordini
parziali (reti di Petri) di sistemi concorrenti. Semantica osservazionale, nozioni di equivalenza fra processi, bisimulazione. - La specifica di proprietà e la loro verifica (logiche modali e temporali, algoritmi di model-checking). Linear Temporal Logic (LTL), Computation Tree Logic (CTL), cenni al calcolo mu.
Prerequisiti
Nozioni di base di programmazione imperativa; nozioni di base di logica proposizionale.
Modalità didattica
Corso erogato in italiano. Lezioni frontali (3 CFU, 24 ore) e esercitazioni in aula (3 CFU, 30 ore).
Materiale didattico
Dispense e articoli pubblicati sul sito dell'insegnamento. Testi di consultazione indicati sul sito dell'insegnamento.
Periodo di erogazione dell'insegnamento
Primo semestre
Modalità di verifica del profitto e valutazione
La valutazione di questo modulo comprende una prova scritta con esercizi su tutte le parti del programma, e un colloquio, con discussione della prova scritta e domande sugli argomenti del modulo. La valutazione è complessiva e definita dopo il colloquio.
Orario di ricevimento
Luca Bernardinello: per appuntamento.
Lucia Pomello: per appuntamento.
Aims
Acquire the ability to formally specify, model, and analyze concurrent systems; acquire the ability to state properties of concurrent systems by means of temporal logics.
Contents
Theoretical tools useful to understand and manipulate basic notions of computer science, related to the behaviour and the specification of distributed and concurrent processes. Fundamental notions about verifying properties of programs ans models of systems. Use of formal logics to specify properties of systems.
Detailed program
- Formal models for specifying and verifying the correctness of programs. Axiomatic semantics of sequential programs, Hoare logic; proofs of correctness of sequential programs.
- Models of concurrency: models of reactive systems, process calculi (CCS, Calculus of Communicating Systems), Petri nets. Fundamental notions about concurrent systems: causal dependence and independence, conflict, confusion, synchronization.
- Interleaving semantics (transition systems) of concurrent systems; partial order semantics (Petri nets). Semantics based on observation, equivalence notions for processes, bisimulation.
- Specification and verification of properties (modal and temporal logics, algorithms for model-checking). Linear Temporal Logic (LTL), Computation Tree Logic (CTL), basic notions of the mu-calculus.
Prerequisites
Basic notions of imperative programming; basic notions of propositional logic.
Teaching form
In Italian language. Lectures (3 CFU, 24 hours) and practice sessions (3 CFU, 30 hours).
Textbook and teaching resource
Notes and papers available on the course site. Reference texts suggested on the course site.
Semester
First semester.
Assessment method
The evaluation for this module includes a written exam with assignments on all sections of the programme, and an oral exam, with discussion of the written part, and questions on the subjects of the module. The score is defined after the discussion.
Office hours
Luca Bernardinello: on appointment.
Lucia Pomello: on appointment.