Differenze

Queste sono le differenze tra la revisione selezionata e la versione attuale della pagina.

--- magistraleinformatica:mvs:start [09/05/2013 alle 14:24 (13 anni fa)] – [Lezioni] Andrea Corradini
+++ magistraleinformatica:mvs:start [23/05/2013 alle 14:39 (13 anni fa)] (versione attuale) – [Metodi per la Verifica del Software (A.A. 2012/13)] Andrea Corradini
@@ Linea 2: / Linea 2: @@
+----
+**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]]
@@ Linea 42: / Linea 45: @@
 |  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 |Verifica di proprietà con SPIN| {{:magistraleinformatica:mvs:mvs-spin-04.pdf}}, {{:magistraleinformatica:mvs:mvs-spin-05.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 |  |   |   |
+|  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 |  |   |   |
+|  21| 16-05-2013 |Esercitazione su PROMELA e SPIN  |   |   |
-|  22| 21-05-2013 |  |   |   |
+|  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 |  |   |   |
+|  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]]**