Metodi per la Verifica del Software (A.A. 2012/13)

Attenzione: Il corso di MVS non sarà erogato nell'Anno Accademico 2013/14, ma sarà erogato regolarmente nell'A.A. 2014/15.

Docente: Andrea Corradini

Corso	Giorno	Ora	Aula
Lezione	Martedì	14-16	C
Lezione	Giovedì	14-16	N1 B

Ricevimento: su appuntamento via email (andrea [at] di [dot] unipi [dot] it)

Materiale Didattico

Slide delle lezioni, che verranno pubblicate di volta in volta.
Christel Baier, Joost Peter Katoen, Principles of Model Checking, MIT Press, 2008
Mordechai Ben-Ari, Principles of the Spin Model Checker, Springer, 2008

Lezioni

N	Data	Argomento	Slide	Altro
1	19-02-2013	Introduzione al corso	lec1.pdf	Schema Model Checking
2	21-02-2013	Sistemi di transizione, Program graphs	lec2.pdf	Def. Transition System, TS per Circuiti Sequenziali, Def. Program Graph, Semantica TS di Program Graphs, Sintassi di GCL
3	28-02-2013	Composizione parallela di sistemi, Channel systems	lec3.pdf, lec4.pdf fino a pag. 51	Def. Interleaving di TS, Mutua esclusione con semaforo, Algoritmo di Peterson, Message-passing sincrono, Def. Channel System, Regole SOS per message-passing asincrono, Regole SOS per message-passing sincrono
4	5-03-2013	Alternating Bit Protocol, Composizione sincrona	lec4.pdf	Esercizi proposti
5	12-03-2013	Proprietà Linear Time	lec5.pdf fino a pag. 159
6	14-03-2013	Invariant and Safety Properties	lec5.pdf e lec6-safety.pdf
7	19-03-2013	Liveness Properties	lec7.pdf fino a pag. 44
8	21-03-2013	Fairness	lec7.pdf
9	26-03-2013	Model Checking Regular Safety Properties	lec08.pdf
10	28-03-2013	Omega Regular Properties	lec09_10.pdf fino a pag. 179	Esercizi proposti
11	9-04-2013	Generalized Büchi Automata, Model Checking with Büchi Automata	lec09_10.pdf, lec11.pdf
12	11-04-2013	Linear Time Logic	lec12_13.pdf fino a pag. 242 (escluso Fairness)
13	16-04-2013	Esercitazione		Correzione esercizi del 28-03-2013
14	18-04-2013	SPIN: Introduzione all'ambiente e PROMELA	mvs-spin-01.pdf, mvs-spin-02.pdf fino a pag. 24
15	23-04-2013	Fairness e LTL; SPIN: Introduzione all'ambiente e PROMELA	lec12_13.pdf, mvs-spin-02.pdf fino a pag. 29	Esercizi suggeriti su SPIN/PROMELA: http://spinroot.com/spin/Man/Exercises.html
16	30-04-2013	LTL Model Checking	lec14_15.pdf, escluso dimostrazione finale
17	2-05-2013	SPIN: Costrutti di controllo di PROMELA	mvs-spin-02.pdf, mvs-spin-03.pdf
18	7-05-2013	Complessità di LTL model checking	lec16.pdf
19	9-05-2013	Specifica di proprietà in PROMELA: asserzioni, end/progress/accept states, never claims	mvs-spin-04.pdf, mvs-spin-2013-05.pdf fino a pag. 11
20	14-05-2013	PROMELA: cenni su trace/notrace assertions, temporal logic patterns, LTL vs ω-regular expressions, semantica operazionale, algoritmi di ricerca, complessità	mvs-spin-2013-05.pdf, mvs-spin-2013-06.pdf	Semantica operazionale di Promela: caltech14.pdf. NB: aggiunti lucidi con nuova sintassi per LTL, da Spin v6, e possibilità di inserire formule LTL inline, senza generare never-claims (vedi MVS-05 p. 17, 18 e 25)
21	16-05-2013	Esercitazione su PROMELA e SPIN
22	21-05-2013	Lezione di Alberto Lluch Lafuente	mvs-spin-2013-07-optimization.pdf	Lucidi di Holzmann su Model Extraction da C code caltech18.ppt. http://spinroot.com/modex/
23	23-05-2013	Overview su CTL e CTL*, Presentazione progetto	lec17-ctl-ctlstar-summary-2013.pdf

Anni precedenti

Anno Accademico 2010/11