Differences

This shows you the differences between two versions of the page.

--- didattica:magistrale:rsv:ay_1516:main [2016/04/15 14:47]
luca [Assignments / Projects]
+++ didattica:magistrale:rsv:ay_1516:main [2020/09/17 16:55] (current)
@@ Line 23: / Line 23: @@
 **Office hours**:
-  * Luca Tesei's office hours are every Wednesday from 11 am to 1 pm in room CS 07, second floor of Polo Tecnologico Palazzo Battibocca, via del Bastione 1, Camerino. For any variation, first look [[http://docenti.unicam.it/pdett.aspx?ids=N&tv=d&UteId=572&ru=RU|here]]
+  * <del>Luca Tesei's office hours are every Wednesday from 11 am to 1 pm in room CS 07, second floor of Polo Tecnologico Palazzo Battibocca, via del Bastione 1, Camerino. For any variation, first look [[http://docenti.unicam.it/pdett.aspx?ids=N&tv=d&UteId=572&ru=RU|here]]</del>
+  * From 13th June 2016 Luca Tesei's office hours schedule can be found [[http://docenti.unicam.it/pdett.aspx?ids=N&tv=d&UteId=572&ru=RU|here]].
   * Prof. Franco Raimondi will be available during his visiting period at Palazzo Battibocca (precise office hours will be communicated)
 </WRAP>
@@ Line 102: / Line 103: @@
    * <del>Wed 27/04/2016 5pm-7pm</del> Thu 28/04/2016 3pm-5pm Prof. Tesei
    * <del>Wed 04/05/2016 5pm-7pm</del> Thu 05/05/2016 3pm-5pm Prof. Tesei
-   * From Thu 12/05/2016 to Fri 27/05/2016 Prof. Raimondi will give 21 hours of lectures - Precise schedule will be communicated
+From Thu 12/05/2016 to Wed 25/05/2016 **Prof. Franco Raimondi** will give the following lectures:
+   * Thu 12/05/2016 3pm-7pm Room D. M. Ritchie
+   * Fri 13/05/2016 11am-1pm Room D. M. Ritchie
+   * Mon 16/05/2016 5pm-7pm Room D. M. Ritchie
+   * Tue 17/05/2016 5pm-7pm Room R. Milner
+   * Thu 19/05/2016 3pm-7pm Room D. M. Ritchie
+   * Mon 23/05/2016 3pm-6pm Room D. M. Ritchie
+   * Tue 24/05/2016 5pm-7pm Room R. Milner
+   * Wed 25/05/2016 5pm-7pm Room D. M. Ritchie
 </WRAP>
@@ Line 137: / Line 147: @@
   * {{:didattica:magistrale:rsv:ay_1516:linear_time_properties._fairness.pdf|Linear Time Properties. Fairness.}} - 6th April 2016
   * {{:didattica:magistrale:rsv:ay_1516:linear_time_properties._regular_safety_properties.pdf|Linear Time Properties. Regular Safety Properties.}} - 7th April 2016 (Partial), 14th April 2016
-  * {{:didattica:magistrale:rsv:ay_1516:linear_time_properties._omega-regular_properties.pdf|Linear Time Properties. Omega-Regular Properties.}} - 14th April 2016 (Partial)
+  * {{:didattica:magistrale:rsv:ay_1516:linear_time_properties._omega-regular_properties.pdf|Linear Time Properties. Omega-Regular Properties.}} - 14th April 2016 (Partial), 21st April 2016
+  * {{:didattica:magistrale:rsv:ay_1516:linear-time-properties._model_checking_with_buchi_automata.pdf|Model Checking with Buchi Automata}} - 28th April 2016
 //Exercises on Linear Time Properties//
   * {{:didattica:magistrale:rsv:ay_1516:mc1516exsollineartime.pdf|Exercises with (some) solutions on Linear Time Properties, Safety/Liveness, Fairness}} - 31st March 2016, 6th April 2016, 7th April 2016
+  * {{:didattica:magistrale:rsv:ay_1516:mc1516exsolregualrproperties.pdf|Exercises with (some) solutions on Regular Properties}} - 28th April 2016 (Partial), 5th May 2016
+  * {{:didattica:magistrale:rsv:ay_1516:mc1516exsolltl-partial.pdf|Exercises with (some) solutions on LTL (Partial overlap with the second part of the course)}}
 //Linear Temporal Logic//
-  * ...
+  * {{:didattica:magistrale:rsv:ay_1516:slides-intro.pdf|Revision of propositional and predicate logic with examples of SAT solvers}} - 13 May 2016
+  * {{:didattica:magistrale:rsv:ay_1516:slides-ltl.pdf|LTL syntax and semantics}} - 13 May 2016
+  * {{:didattica:magistrale:rsv:ay_1516:slides-ltl2buchi.pdf|LTL to Buchi}} - 16 May 2016
 //Exercises on Linear Temporal Logic//
-  * ...
+  * {{:didattica:magistrale:rsv:ay_1516:exercise-sheet.pdf|LTL exercises}}
+//Computational Tree Logic//
+  * {{:didattica:magistrale:rsv:ay_1516:slides-ctl.pdf|CTL syntax and semantics}} - 17 May 2016
+  * {{:didattica:magistrale:rsv:ay_1516:slides-mcctl.pdf|CTL model checking and OBDDs}} - 19 May 2016
+//Tools and practical applications//
+  * {{:didattica:magistrale:rsv:ay_1516:slides-nusmv.pdf|NuSMV}} - 23 May 2016
+  * {{:didattica:magistrale:rsv:ay_1516:slides-spin.pdf|Spin}} - 23 May 2016
+  * {{:didattica:magistrale:rsv:ay_1516:slides-jpf.pdf|JPF}} - 24 May 2016
+  * {{:didattica:magistrale:rsv:ay_1516:slides-smt.pdf|SMT, Z3, Concolic testing, DO178}} - 25 May 2016
 **Reference books**
   * Christel Baier, Joost-Pieter Katoen, “Principles of Model Checking”, The MIT Press, 2008, ISBN: 9780262026499. Website of the book with additional material available [[http://mitpress.mit.edu/books/principles-model-checking|here]]
   * Michael Huth, Mark Ryan, "Logic in Computer Science", Second Edition, Cambridge University Press, 2004. ISBN: 9780521543101.
-  * Lecture notes and slides may be given by the teachers for studying and for exercises. These can be download from the section above
+  * Lecture notes and slides may be given by the teachers for studying and for exercises. These can be downloaded from the section above
 **Other Books**
@@ Line 161: / Line 186: @@
 <WRAP box round center 95%>
 **Assignments:**
-  * {{:didattica:magistrale:rsv:ay_1516:rsv1516-assignment_1.pdf|Text of Assignment 1}}. Deadline to return the homework by email is **Friday 29th April 2016 at 23.59**
+  * {{:didattica:magistrale:rsv:ay_1516:rsv1516-assignment_1.pdf|Text of Assignment 1}}. Deadline to return the homework by email is **Friday 29th April 2016 at 23.59** - [[https://dl.dropboxusercontent.com/u/33462615/RSV1516-Assignment-1-Solution.pdf|Solutions]]
+  * {{:didattica:magistrale:rsv:ay_1516:assignment_franco.pdf|Text of Assignment 2}}. Deadline to return the homework by email is **Friday 10th June 2016 at 23.59** - Solutions not available yet.
+  * {{:didattica:magistrale:rsv:ay_1516:rsv1516-assignment-3.pdf|Text of Assignment 3}}. Deadline to return the homework by email is **Friday 24th June 2016 at 23.59** - {{:didattica:magistrale:rsv:ay_1516:rsv1516-assignment-3-solution.pdf|Solutions}}
 </WRAP>