Differences

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

--- didattica:magistrale:rsv:ay_1516:main [2016/05/13 12:49]
franco
+++ 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 152: / Line 153: @@
   * {{: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**
@@ Line 173: / 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>