~~NOTOC~~

====== Weekly Calendar ======

===== January 4 =====

//Title:// Bugs are everywhere\\
//Reading material:// page 1-2, 4-6 of the textbook\\
//Slides:// {{:public:lecture1.pdf|lecture1.pdf}}

===== January 5 =====

//Title:// Testing on steriods\\
//Reading material:// [[http://junit.org|JUnit website]]\\
//Slides:// {{:public:lecture2.pdf|lecture2.pdf}}

===== January 7 =====

//Lab:// [[lab1|Lab1]]

===== January 11 =====

//Title:// Concurrency\\
//Reading material:// [[https://docs.oracle.com/javase/tutorial/essential/concurrency/|The Java Tutorials: Concurrency]]\\
//Slides:// {{:public:lecture3.pdf|lecture3.pdf}}\\
//Code:// {{:public:Byte.txt|Byte.java}}, {{:public:ByteTest.txt|ByteTest.java}}, {{:public:Printer-Thread.txt|Printer.java (using Thread)}}, {{:public:TwoPrinters-Thread.txt|TwoPrinters.java (using Thread)}}. {{:public:Printer-Runnable.txt|Printer.java (using Runnable)}}. {{:public:TwoPrinters-Runnable.txt|TwoPrinters.java (using Runnable)}}

===== January 12 =====

//Title:// States and transitions\\
//Reading material:// Section 2.3 of the textbook\\
//Slides:// {{:public:lecture4.pdf|lecture4.pdf}}

===== January 14 =====

//Reading material:// {{:public:chapter1-2.pdf|Notes}}\\
//Lab:// [[lab2|Lab2]]

===== January 18 =====

//Title:// Model Checking\\
//Reading material:// page 3, 7-10 of the textbook, [[https://docs.oracle.com/javase/tutorial/essential/concurrency/|The Java Tutorials: Concurrency]]\\
//Slides:// {{:public:lecture5.pdf|lecture5.pdf}}\\
//Code:// {{:public:Counter.txt|Counter.java}}, {{:public:Resource.txt|Resource.java}}

===== January 19 =====

//Title:// Smaller Models\\
//Reading material:// \\
//Slides:// {{:public:lecture6.pdf|lecture6.pdf}}\\
//Code:// {{:public:Semaphore.txt|Semaphore.java}}, {{:public:AtomicInteger.txt|AtomicInteger.java}}

===== January 21 =====

//Reading material:// [[https://docs.oracle.com/javase/tutorial/essential/concurrency/|The Java Tutorials: Concurrency]]\\
//Lab:// [[lab3|Lab3]]

===== January 25 =====

//Title:// Introduction to Java PathFinder\\
//Reading material:// [[http://dx.doi.org.ezproxy.library.yorku.ca/10.1007/3-540-48234-2_11|Java PathFinder: a translator from Java to Promela]]\\
//Slides:// {{:public:lecture7.pdf|lecture7.pdf}}

===== January 26 =====

//Title:// Deadlocks and Race Conditions\\
//Reading material:// Section 3.1 of the textbook\\
//Slides:// {{:public:lecture8.pdf|lecture8.pdf}}\\
//Code:// {{:public:Locker.txt|Locker.java}}, {{:public:TwoLockers.txt|TwoLockers.java}}, {{:public:Friend.txt|Friend.java}}, {{:public:TwoFriends.txt|TwoFriends.java}}

===== January 28 =====

//Lab:// [[lab4|Lab4]]

===== February 1 =====

//Title:// Listeners\\
//Reading material:// [[https://docs.oracle.com/javase/tutorial/uiswing/events/|The Java Tutorials: Writing Event Listeners]]\\
//Slides:// {{:public:lecture9.pdf|lecture9.pdf}}\\
//Code:// {{:public:Generator.txt|Generator.java}}, {{:public:Listener.txt|Listener.java}}, {{:public:ListenerAdapter.txt|ListenerAdapter.java}}, {{:public:Main.txt|Main.java}}, {{:public:PlusPrinter.txt|PlusPrinter.java}}, {{:public:StarPrinter.txt|StarPrinter.java}}, {{:public:SumPrinter.txt|SumPrinter.java}}, {{:public:ValuePrinter.txt|ValuePrinter.java}}

===== February 2 =====

//Title:// Listeners in JPF\\
//Reading material:// Chapter 4 of {{:public:chapter1-5.pdf|Notes}}, [[http://wuyongzheng.github.io/jpfdoc/gov/nasa/jpf/listener/package-summary.html|JPF API]]\\
//Slides:// {{:public:lecture10.pdf|lecture10.pdf}}\\
//Code:// {{:public:garbage-1.txt|Garbage.java (prints *)}}, {{:public:garbage-2.txt|Garbage.java (timer)}}, {{:public:statespace-1.txt|StateSpace.java (txt version)}},{{:public:statespace-2.txt|StateSpace.java (dot version)}}, {{:public:statespace-3.txt|StateSpace.java (dot version with colours)}}

===== February 4 =====

//Lab:// [[lab5|Lab5]]

===== February 8 =====

//Title:// Search Strategies in JPF\\
//Reading material:// Chapter 5 of {{:public:chapter1-5.pdf|Notes}}\\
//Slides:// {{:public:lecture11.pdf|lecture11.pdf}}\\
//Code:// {{:public:DFSearch.txt|DFSearch.java}}

===== February 9 =====

//Speaker:// Julia Rubin\\
//Title:// The Secret Life of Mobile Applications\\
//Location:// Lassonde Building, room 3033\\
//Time:// 14:00-15:00

===== February 11 =====

//Lab:// [[lab6|Lab6]]

===== February 22 =====

//Title:// Handling Native Methods (Model Classes)\\
//Reading material:// \\
//Slides:// {{:public:lecture13.pdf|lecture13.pdf}}\\
//Code:// {{:public:Sine.txt|Sine.java}}, {{:public:StrictMath.txt|StrictMath.java}}

===== February 23 =====

//Title:// Handling Native Methods (Native Peers)\\
//Reading material:// \\
//Slides:// {{:public:lecture14.pdf|lecture14.pdf}}\\
//Code:// {{:public:JPF_java_lang_StrictMath.txt|JPF_java_lang_StrictMath.java}}

===== February 25 =====

//Lab:// [[lab7|Lab7]]

===== February 29 =====

//Title:// The State Space in XML Format\\
//Reading material:// \\
//Slides:// {{:public:lecture15.pdf|lecture15.pdf}}\\
//Code:// {{:public:StateSpacePrinter-2.txt|StateSpacePrinter.java}}

===== March 1 =====

//Title:// Linear Temporal Logic\\
//Reading material:// pages 229-236 of the textbook\\
//Slides:// {{:public:lecture16.pdf|lecture16.pdf}}\\

===== March 3 =====

//Lab:// [[lab8|Lab8]]

===== March 7 =====

//Title:// Linear Temporal Logic\\
//Reading material:// pages 237-249 of the textbook\\
//Slides:// {{:public:lecture17.pdf|lecture17.pdf}}

===== March 8 =====

//Title:// Linear Temporal Logic\\
//Reading material:// pages 252, 255-256, 313-327, 334-340 of the textbook\\
//Slides:// {{:public:lecture18.pdf|lecture18.pdf}}\\

===== March 10 =====

//Lab:// work on your project and quiz on Linear Temporal Logic

===== March 14 =====

//Title:// Computation Tree Logic\\
//Reading material:// pages 341-351 of the textbook and {{:public:partialorder.pdf|note on partial ordered sets and fixed points}}\\
//Slides:// {{:public:lecture19.pdf|lecture19.pdf}}

===== March 15 =====

//Title:// Witnesses and Counterexamples\\
//Reading material:// pages 373-379 of the textbook\\
//Slides:// {{:public:lecture20.pdf|lecture20.pdf}}\\
//Code:// {{:public:MaggieDogPoissonProblem.txt|MaggieDogPoisonProblem.java}}

===== March 17 =====

//Lab:// work on your project and quiz on Computation Tree Logic

===== March 21 =====

//Title:// Software for Dependable Systems\\
//Reading material:// [[http://www.nap.edu/catalog/11923/software-for-dependable-systems-sufficient-evidence|Software for Dependable Systems: Sufficient Evidence?]]\\
//Slides:// {{:public:lecture21.pdf|lecture21.pdf}}

===== March 22 =====

Course evaluations (please bring a pencil)

//Title:// Structured Proofs\\
//Reading material:// [[http://dx.doi.org.ezproxy.library.yorku.ca/10.1007/s11784-012-0071-6|How to write a 21st century proof]]\\
//Slides:// {{:public:lecture22.pdf|lecture22.pdf}}

===== March 24 =====

Lab cancelled due to weather.

===== March 28 =====

Quiz

//Title:// Binary Decision Diagrams\\
//Reading material:// pages 382-386, 392-405 of the textbook\\
//Slides:// {{:public:lecture23.pdf|lecture23.pdf}}

===== March 29 =====

//Title:// Binary Decision Diagrams\\
//Reading material:// pages 387-391 of the textbook\\
//Slides:// {{:public:lecture24.pdf|lecture24.pdf}}

===== March 31 =====

//Lab:// work on your project and quiz

===== April 4 =====

Make up lab at 14:30.

===== April 11 =====

Final exam at 14:00-16:00 in ACE 006

===== April 15 =====

Last day to hand in your project