Metodi formali

A.A. 2015/2016
Insegnamento per
6
Crediti massimi
48
Ore totali
Lingua
Italiano

Struttura insegnamento e programma

Edizione attiva
Responsabile
STUDENTI FREQUENTANTI
Programma
il corso è suddiviso in due tronconi paralleli che affrontano diverse tematiche legate alla verifica formale

Parte A: Model Checking e Logiche Temporali

· Motivazioni: il model-checking come strumento totalmente automatico per la verifica del comportamento di sistemi reattivi e concorrenti.
· La logiche temporali LTL e CTL: sintassi e semantica, confronto di espressività, assiomatizzazione (cenni), forme normali negative.
· Model-checking: introduzione al problema con esempi tratti dai corsi di sistemi operativi e reti (mutua esclusione, produttore/consumatore, cena dei filosofi, ecc.).
· Automi su parole infinite: automi di Buchi e linguaggi omega-regolari, automi vuoti e chiusura booleana.
· Soddisfacibilità e model-checking esplicito in LTL: insiemi di Hintikka, formule e automi, tableaux per LTL.
· Punti fissi di operatori monotoni: teorema di Knaster-Tarski, applicazione agli operatori di CTL.
· Model-checking simbolico in CTL: macchine a stati finiti, OBDD (`ordered binary decision diagrams'), simulazione simbolica dell'approssimazione dei punti fissi.
· Model-checking limitato: la riduzione a SAT e l'utilizzo dei SAT-solver nel model-checking.
· Model-checking per sistemi a stati infiniti: well-structured systems e algoritmi di raggiungibilità a ritroso; la tecnica del modello approssimato e il modello `stopping failures';
· Model-checking per sistemi a stati infiniti: sviluppi recenti per un approccio dichiarativo tramite SMT-solvers.; array-based systems; esempi tratti da protocolli di mutua esclusione, protocolli di cache coherence, canali con perdita di informazione, fault-tolerant systems, automi temporizzati parametrici.
· Supporto software: introduzione alla sintassi dei sistemi NuSMV (per sistemi a stati finiti) e MCMT (per sistemi a stati infiniti).

Parte B: Software Foundations con Coq

In questa parte esploreremo delle tecniche formali per migliorare l'affidabilità del software, concentrandoci in particolare sulla specifica e dimostrazione di proprietà dei programmi.

La particolarità di questa parte è di essere costruita interamente all'interno di Coq, uno dei proof assistant (p.a.) più maturi ed usati. Un p.a. è un dimostratore di teoremi interattivo, che cioè automatizza gli aspetti più di routine della dimostrazione ma dipende dall'utente per la strategia dimostrativa.

Il corso, esercizi compresi, va quindi (e)seguito come una sessione interattiva con il sistema. Gli argomenti principali che svilupperemo saranno:

(1) (Ri)esame di alcuni strumenti basi logici per la specifica e dimostrazione delle proprietà di interesse (induzione, ricorsione, riscrittura).

(2) Uso dei p.a. nella costruzione di argomenti logici rigorosi.

(3) La programmazione funzionale sia come metodologia di programmazione che come ponte con la logica.

(4) Tecniche formali per il ragionamenti sulle proprietà di programmi
specifici (e.g. terminazione di un loop, dimostrazione che una funzione di
oridnamento soddisfa la sua specifica) e

(5) per la dimostrazione di proprietà di tutti i programmi di un certo
linguaggio, attraverso l'uso di sistemi di tipi.
Propedeuticità
logica matematica
Prerequisiti e modalità di esame
Conoscenze elementari di logica.
Metodi didattici
misti (videolezioni)
Materiale didattico e bibliografia
Parte A:
dispense disponibili sul sito del corso;
- Clarke, Grumberg, Peled, Model Checking, MIT Press, 2000.
- materiali vari disponibili sui siti di NuSMV e MCMT.

Parte B
- online book Software Foundations.
- Testi supplementari:
-- Types and Programming Languages (Pierce).
-- Interactive Theorem Proving and Program Development, by Yves Bertot and Pierre Castàran
STUDENTI NON FREQUENTANTI
Programma
da stabilire con i docenti
Prerequisiti e modalità di esame
Conoscenze elementari di logica.
Materiale didattico e bibliografia
da stabilirsi con i docenti
Periodo
Primo semestre
Periodo
Primo semestre
Modalità di valutazione
Esame
Giudizio di valutazione
voto verbalizzato in trentesimi
Siti didattici
Docente/i
Ricevimento:
venerdì alle 11,30
Dipartimento di Matematica, via C. Saldini 50
Ricevimento:
venerdì 14.30--16
4009