Metodi formali

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:
In questa parte esploreremo delle tecniche formali per migliorare
l'affidabilità del software, concentrandoci in particolare sulla
specifica e dimostrazione di proprietà del software.

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. è uno esempio di 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 ed esame compresi, va quindi (e)seguito come una sessione
interattiva con il sistema.
(http://www.seas.upenn.edu/~cis500/current/sf/index.html)

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 (terminazione di un loop, dimostrazione che una funzione di
sorting 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.