Differenze

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

--- magistraleinformatica:mvs:start [30/04/2013 alle 16:15 (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 40: / Linea 43: @@
 |  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 |  |   |   |
+|  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 |  |   |   |
+|  18| 7-05-2013 |Complessità di LTL model checking | {{:magistraleinformatica:mvs:lec16.pdf|}}  |   |
-|  19| 9-05-2013 |  |   |   |
+|  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]]**