====== 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: [[http://www.di.unipi.it/~andrea/|Andrea Corradini]]

^ Corso ^ Giorno ^  Ora  ^  Aula  ^
| Lezione | Martedì|  14-16  |  C  | 
| Lezione | Giovedì |  14-16  |  <del>N1</del>   B  |


Ricevimento: su appuntamento via email (<andrea@di.unipi.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 | {{:magistraleinformatica:mvs:lec1.pdf}} | {{:magistraleinformatica:mvs:01-model-checking-overview.pdf|Schema Model Checking}}   | 
|  2| 21-02-2013 | Sistemi di transizione, Program graphs | {{:magistraleinformatica:mvs:lec2.pdf}} | {{:magistraleinformatica:mvs:02-def-transition-system.pdf|Def. Transition System}},  {{:magistraleinformatica:mvs:03-ts-for-sequential-circuits.pdf|TS per Circuiti Sequenziali}}, {{:magistraleinformatica:mvs:04-def-program-graph.pdf|Def. Program Graph}}, {{:magistraleinformatica:mvs:05-ts-semantics-of-program-graphs.pdf|Semantica TS di Program Graphs}}, {{:magistraleinformatica:mvs:06-syntax-of-guarded-command-lang.pdf|Sintassi di GCL}}   |
|  3| 28-02-2013 | Composizione parallela di sistemi, Channel systems | {{:magistraleinformatica:mvs:lec3.pdf}}, {{:magistraleinformatica:mvs:lec4.pdf}} fino a pag. 51 | {{:magistraleinformatica:mvs:07-def-interleaving-of-ts.pdf|Def. Interleaving di TS}}, {{:magistraleinformatica:mvs:08-mutual-exclusion-with-semaphore.pdf|Mutua esclusione con semaforo}}, {{:magistraleinformatica:mvs:09-peterson-algorithm.pdf|Algoritmo di Peterson}}, {{:magistraleinformatica:mvs:10-def-synchronous-message-passing.pdf|Message-passing sincrono}}, {{:magistraleinformatica:mvs:11-def-channel-system.pdf|Def. Channel System}}, {{:magistraleinformatica:mvs:12-sos-rules-asynchronous-message-passing.pdf|Regole SOS per message-passing asincrono}}, {{:magistraleinformatica:mvs:13-sos-rules-synchronous-message-passing.pdf|Regole SOS per message-passing sincrono}}   |
|  4| 5-03-2013 |Alternating Bit Protocol, Composizione sincrona | {{:magistraleinformatica:mvs:lec4.pdf}} | {{:magistraleinformatica:mvs:esercizi-2013-01.pdf|Esercizi proposti}}   |
|  5| 12-03-2013 |Proprietà Linear Time | {{:magistraleinformatica:mvs:lec5.pdf}} fino a pag. 159 |     | 
|  6| 14-03-2013 |Invariant and Safety Properties| {{:magistraleinformatica:mvs:lec5.pdf}} e {{:magistraleinformatica:mvs:lec6-safety.pdf}} |     |     
|  7| 19-03-2013 |Liveness Properties| {{:magistraleinformatica:mvs:lec7.pdf}} fino a pag. 44 |     |  
|  8| 21-03-2013 |Fairness | {{:magistraleinformatica:mvs:lec7.pdf}} |     |  
|  9| 26-03-2013 |Model Checking Regular Safety Properties | {{:magistraleinformatica:mvs:lec08.pdf}} |     |  
|  10| 28-03-2013 |Omega Regular Properties | {{:magistraleinformatica:mvs:lec09_10.pdf}} fino a pag. 179| {{:magistraleinformatica:mvs:esercizi-2013-02.pdf|Esercizi proposti}}  |  
|  11| 9-04-2013 | Generalized Büchi Automata, Model Checking with Büchi Automata | {{:magistraleinformatica:mvs:lec09_10.pdf}}, {{:magistraleinformatica:mvs:lec11.pdf}}|  |  
|  12| 11-04-2013 |Linear Time Logic | {{:magistraleinformatica:mvs: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| {{:magistraleinformatica:mvs:mvs-spin-01.pdf}}, {{:magistraleinformatica:mvs:mvs-spin-02.pdf}} fino a pag. 24|     | 
|  15| 23-04-2013 |Fairness e LTL; SPIN: Introduzione all'ambiente e PROMELA| {{:magistraleinformatica:mvs:lec12_13.pdf}}, {{:magistraleinformatica:mvs: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| {{:magistraleinformatica:mvs:lec14_15.pdf}}, escluso dimostrazione finale|   | 
|  17| 2-05-2013 |SPIN: Costrutti di controllo di PROMELA|{{:magistraleinformatica:mvs:mvs-spin-02.pdf}}, {{:magistraleinformatica:mvs:mvs-spin-03.pdf}}|   | 
|  18| 7-05-2013 |Complessità di LTL model checking | {{:magistraleinformatica:mvs:lec16.pdf|}}  |   | 
|  19| 9-05-2013 |Specifica di proprietà in PROMELA: asserzioni, end/progress/accept states, never claims| {{:magistraleinformatica:mvs:mvs-spin-04.pdf}}, {{:magistraleinformatica:mvs: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à |{{:magistraleinformatica:mvs:mvs-spin-2013-05.pdf}}, {{:magistraleinformatica:mvs:mvs-spin-2013-06.pdf}}   |Semantica operazionale di Promela: {{:magistraleinformatica:mvs: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 [[http://www.albertolluch.com/|Alberto Lluch Lafuente]]  |  {{:magistraleinformatica:mvs:mvs-spin-2013-07-optimization.pdf|}} | Lucidi di Holzmann su Model Extraction da C code {{:magistraleinformatica:mvs:caltech18.ppt|caltech18.ppt}}. http://spinroot.com/modex/  | 
|  23| 23-05-2013 | Overview su CTL e CTL*, Presentazione progetto | {{:magistraleinformatica:mvs:lec17-ctl-ctlstar-summary-2013.pdf|}}  |   | 
===== Anni precedenti  =====

**[[.:year2010:start|Anno Accademico 2010/11]]**