diff --git a/anno3/vpc/00.19-20Intro-Corso.pdf b/anno3/vpc/00.19-20Intro-Corso.pdf
new file mode 100644
index 0000000..b17a0a0
Binary files /dev/null and b/anno3/vpc/00.19-20Intro-Corso.pdf differ
diff --git a/anno3/vpc/01.19-20AnalisiRdP-PAnoAnimazioni.pdf b/anno3/vpc/01.19-20AnalisiRdP-PAnoAnimazioni.pdf
new file mode 100644
index 0000000..97b08a2
Binary files /dev/null and b/anno3/vpc/01.19-20AnalisiRdP-PAnoAnimazioni.pdf differ
diff --git a/anno3/vpc/02.19-20WN.pdf b/anno3/vpc/02.19-20WN.pdf
new file mode 100644
index 0000000..5208182
Binary files /dev/null and b/anno3/vpc/02.19-20WN.pdf differ
diff --git a/anno3/vpc/03.19-20PN.pdf b/anno3/vpc/03.19-20PN.pdf
new file mode 100644
index 0000000..11c60de
Binary files /dev/null and b/anno3/vpc/03.19-20PN.pdf differ
diff --git a/anno3/vpc/03.b.19-020PNridotto.pdf b/anno3/vpc/03.b.19-020PNridotto.pdf
new file mode 100644
index 0000000..52957cb
Binary files /dev/null and b/anno3/vpc/03.b.19-020PNridotto.pdf differ
diff --git a/anno3/vpc/Amparore-Donatelli2018_Chapter_GreatTeachAToolForTeachingStoc.pdf b/anno3/vpc/Amparore-Donatelli2018_Chapter_GreatTeachAToolForTeachingStoc.pdf
new file mode 100644
index 0000000..8e76e5e
Binary files /dev/null and b/anno3/vpc/Amparore-Donatelli2018_Chapter_GreatTeachAToolForTeachingStoc.pdf differ
diff --git a/anno3/vpc/Appunti corso Andy Miner a IOWA state su PN - DD - CTL e LTL.pdf b/anno3/vpc/Appunti corso Andy Miner a IOWA state su PN - DD - CTL e LTL.pdf
new file mode 100644
index 0000000..2f9ded0
Binary files /dev/null and b/anno3/vpc/Appunti corso Andy Miner a IOWA state su PN - DD - CTL e LTL.pdf differ
diff --git a/anno3/vpc/miner-notes.pdf b/anno3/vpc/miner-notes.pdf
new file mode 100644
index 0000000..cd26b2e
Binary files /dev/null and b/anno3/vpc/miner-notes.pdf differ
diff --git a/anno3/vpc/obbiettivi_del_corso b/anno3/vpc/obbiettivi_del_corso
new file mode 100644
index 0000000..6ca11f7
--- /dev/null
+++ b/anno3/vpc/obbiettivi_del_corso
@@ -0,0 +1,7 @@
+Obiettivo del corso e' di fornire gli strumenti, teorici e pratici, necessari alla verifica dei sistemi, ed in particolare del software. Per raggiungere tale obiettivo studieremo alcuni paradigmi di base per la specifica di processi distribuiti, focalizzando l'attenzione sulle capacità modellistiche e sugli strumenti di verifica di proprietà di buon comportamento.
+
+Alla fine del corso lo studente sara' in grado di specificare sistemi concorrenti usando linguaggi formali e di utilizzare strumenti software per la verifica di proprieta' del sistema tramite verifica di proprieta' del modello. Oltre alle classiche proprieta' dei sistemi distribuiti quali assenza di deadlock, fairness e liveness, lo studente sara' in grado di definire e verificare proprieta' in logica temporale quali ad esempio: "se il processo P manda un messaggio, allora non ricevera' il prossimo messaggio sino a che non riceve un acknowledgment", oppure "se il processo P manda un messaggio, ricevera' un acknowledge entro 5 unita' di tempo".
+
+Il corso non ha come obiettivo di fornire conoscenza su strumenti di verifica di linguaggi di programmazione, perche'  non si focalizza sulla verifica dell' implementazione degli algoritmi, ma sulla verifica delle soluzioni algoritmiche legate alla concorrenza.
+Nel ciclo di sviluppo del software le competenze acquisite in questo corso sono utili al fine della progettazione e verifica di soluzioni concorrenti/distribuite
+Ultime modifiche: lunedì, 22 febbraio 2016, 11:06
\ No newline at end of file
diff --git a/anno3/vpc/testi b/anno3/vpc/testi
new file mode 100644
index 0000000..68c6a56
--- /dev/null
+++ b/anno3/vpc/testi
@@ -0,0 +1,13 @@
+Testo su reactive systems (CCS, Equivalenze e Timed Automata)
+
+Il testo "Reactive Systems: Modelling, specification and verification" di Luca Aceto e colleghi e'  un ottimo libro di testo, soprattutto per quanto riguarda la parte su CCS, equivalenze e timed system.
+
+Il pdf dei primi capitoli del libro si trova facilmente in rete, su siti legali (universita'  di appartenenza degli autori http://www.cs.ioc.ee/yik/schools/win2007/ingolfsdottir/sv-book-part1.pdf e ), mentre la versione integrale  stampata e'  disponibile presso la biblioteca del Diaprtimento di Informatica.
+
+Ultime modifiche: lunedì, 2 marzo 2020, 14:08
+
+
+ALTRO:
+
+seven_myths_of_formal_methods
+Teaching Formal Methods for Software Engineering –Ten Principles
\ No newline at end of file
diff --git a/anno3/vpc/verifica_apprendimento b/anno3/vpc/verifica_apprendimento
new file mode 100644
index 0000000..ac907f5
--- /dev/null
+++ b/anno3/vpc/verifica_apprendimento
@@ -0,0 +1,16 @@
+Combinazione di:
+
+Piccoli esercizi e più consistenti progetti durante il corso, con precise date di consegna (pencil and paper and use of tools)
+
+Gli esercizi devono essere accompagnati da una relazione (written report)
+
+Verifica finale – discussione degli esercizi con uso dei tool e verifica della parte di teoria  (dates can be agreed upon with the teacher, contact the teacher at least 10 days before)
+
+Ci sono due modalita’ per la valutazione
+
+Orientata agli strumenti:  sperimentazioni complete con gli strumenti di verifica. Discussione dei laboratori e una prova orale sugli argomenti principali
+
+Orientata alla teoria: esercizi piu’ semplici e classico esame di teoria su tutti gli argomenti del corso
+
+
+Ultime modifiche: lunedì, 22 febbraio 2016, 11:07
\ No newline at end of file