Metodi formali

A.A. 2016/2017
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:
La seconda parte del corso di Metodi Formali e' un minicorso monografico sulla programmazione logica in PROLOG.
Vengono richiamati i fondamenti teorici di logica-matematica e i concetti necessaria comprendere la programmazione logica.
L'insegnamento del linguaggio di programmazione logica PROLOG e' corredato da esercitazioni in laboratorio in cui si usa il PROLOG per implementare programmi per la risoluzione di problemi.
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