Formal Methods
Docente/Lecturer
Prof. Marina Lenisa
Indirizzo e-mail
Indirizzo Pagina Web Personale
http://www.dimi.uniud.it/members/marina.lenisa/
Crediti/Credits
6 CFU
The course is held in English
Objectives
The aim of the course on Formal Methods is to illustrate rigorous tools for the formal verification of program correctness. In particular, the Hoare Logic, based on program invariants, will be presented for the verification of sequential, parallel and distributed programs. Correctness and termination of a number of classical sequential algorithms will be discussed formally, while issues such as deadlock and fairness will be formally analyzed for a number of paradigmatic problems of concurrency.
Programme
- Introduction to the formal verification of program correctness.
- Syntax and operational semantics of deterministic programs.
- Hoare system of rules for the correctness of deterministic programs.
- Completeness of Hoare systems.
- Formal verification of classical sequential algorithms: partial correctness and termination.
- Syntax and operational semantics of parallel disjoint programs.
- Reduction of disjoint parallelism to sequentiality.
- Verification of parallel disjoint programs.
- Verification of parallel programs with shared variables: partial correctness.
- Strong correctness of proof outlines. Rule for parallelism and its incompleteness. Rule for auxiliary variables.
- Total correctness of parallel programs with shared variables.
- Parallel programs with shared variables. Non-compositional behavior of components.
- Parallel programs with synchronization: syntax, operational semantics.
- Correctness of paradigmatic examples of parallel programs with synchronization: partial correctness, termination, deadlock absence.
- Paradigmatic examples of parallel programs with synchronization: producer and consumer, readers and writers, implementation and use of semaphores, etc.
- Non-deterministic programs: syntax, operational semantics, rules for correctness.
- Usefulness of non-deterministic programs. Translations of parallel programs into non-deterministic programs.
- Classical examples: the transmission problem with variants (with or without filtering, with or without acknowledgements, etc).
- Introduction to distributed programming. Syntax, Operational semantics. Translation of distributed programs into non-deterministic programs, and relationships between their semantics.
- Verification of distributed programs: partial correctness, termination, deadlock absence.
- Fairness: study of program correctness under the hypothesis of fair scheduling. The methodology used is based on the implementation of a fair scheduler inside the program itself. Such implementation requires a language extended with random assignment. The proof of termination requires the use of termination functions defined on well-founded structures generalizing natural numbers.
Bibliography
- Lecture slides.
- Apt K., de Boer F., Olderog E-R., "Verification of Sequential and Concurrent Programs", Springer, 3rd edition, 2009.
Exam mode
Written exam + oral exam. The oral part is optional.
**************************************************************************************************
Finalità e obbiettivi formativi
L'obiettivo del corso di Metodi Formali e` quello di fornire allo studente strumenti rigorosi per la verifica formale di correttezza di programmi. In particolare, verra` illustrata la Logica di Hoare, basata su invarianti, per la verifica di programmi sequenziali, paralleli e distribuiti. Si discuteranno formalmente correttezza e terminazione di diversi algoritmi sequenziali classici. Mentre questioni come assenza di deadlock e fairness verranno affrontate formalmente per una serie di problemi paradigmatici di concorrenza.
Programma
- Introduzione alla verifica formale della correttezza di programmi.
- Sintassi e semantica operazionale di programmi deterministici.
- Sistema di regole alla Hoare per la correttezza di programmi deterministici. -Verifica formale di algoritmi sequenziali classici. Correttezza parziale e terminazione.
- Completezza dei sistemi di regole alla Hoare.
- Sintassi e Semantica Operazionale di programmi paralleli disgiunti.
- Riduzione del parallelismo disgiunto alla sequenzialita`.
- Verifica di programmi paralleli disgiunti.
- Verifica di programmi paralleli con variabili condivise: correttezza parziale.
- Correttezza Forte dei proof outline. Regola per il parallelismo e sua incompletezza. Regola per le variabili ausiliarie.
- Correttezza totale di programmi paralleli con variabili condivise.
- Programmi paralleli con variabili condivise. Comportamento non-composizionale delle componenti.
- Programmi paralleli con sincronizzazione: sintassi, semantica operazionale.
- Verifica di correttezza di programmi paralleli con sincronizzazione: correttezza parziale, terminazione, assenza di deadlock.
- Verifica di correttezza di esempi classici di programmi paralleli con sincronizzazione: produttore e consumatore, lettori e scrittori, implementazione e uso di semafori, etc.
- Programmi non-deterministici: sintassi, semantica operazionale, regole per la verifica di correttezza.
- Utilità dei programmi non-deterministici. Traduzione di programmi paralleli in programmi non-deterministici.
- Introduzione alla programmazione distribuita. Programmi distribuiti: sintassi, semantica operazionale.
- Esempi classici: il problema della trasmissione nelle sue varianti (con e senza filtraggio di dati, con e senza messaggi di acknowledgment, etc).
- Traduzione di programmi distribuiti in programmi non-deterministici e relazioni tra le semantiche.
- Verifica: correttezza parziale, terminazione, assenza di deadlock.
- Fairness: studio della correttezza di programmi paralleli sotto l'ipotesi di schedulazione fair. La metodologia presentata si basa sull'implementazione di uno scheduler fair all'interno del programma stesso. Tale implementazione e` definita su un linguaggio esteso con assegnamento random. La prova di terminazione richiede l'utilizzo di funzioni di terminazione definite su strutture ben fondate che generalizzano i naturali.
Prerequisiti
Programmazione e laboratorio (necessario).
Logica Matematica (necessario)
Sistemi Operativi (necessario)
Bibliografia
- Trasparenze usate a lezione
- Apt K., de Boer F., Olderog E-R., "Verification of Sequential and Concurrent Programs", Springer, 3rd edition, 2009.
Modalità d'esame
L'esame è costituito da una prova scritta ed una orale. Quest’ultima è facoltativa.
Orario di ricevimento
Lunedì 10.00-11.00 oppure su appuntamento.