~~NOTOC~~

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

===== January 6 =====

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

===== January 9 =====

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

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

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

===== January 13 =====

//Title:// State exploration\\
//Reading material:// page 3, 7-8, 11-16 of the textbook\\
//Slides:// {{:public:lecture3.pdf|lecture3.pdf}}\\
//Code:// {{:public:Quick.txt|Quick.java}}, {{:public:RandomFraction.txt|RandomFraction.java}}

===== January 16 =====

//Lab:// [[lab2|Lab 2]]\\
//Quiz:// [[quiz1|Quiz 1]]

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

//Title:// Mini Models\\
//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:lecture4.pdf|lecture4.pdf}}\\
//Code:// {{:public:PrintRandom.txt|PrintRandom.java}}, {{:public:RunTest.txt|RunTest.java}}

===== January 20 =====

//Title:// Mini Models\\
//Slides:// {{:public:lecture5.pdf|lecture5.pdf}}\\
//Code:// {{:public:OneChoice.txt|OneChoice.java}}, {{:public:TwoChoices.txt|TwoChoices.java}}

===== January 23 =====

//Reading material:// Chapter 1 of {{:public:notes.pdf|notes.pdf}}\\
//Project:// [[project1|Part 1 of project (5%)]]

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

//Title:// Mini Models\\
//Slides:// {{:public:lecture6.pdf|lecture6.pdf}}\\
//Code:// {{:public:manychoices.txt|ManyChoices.java}}

===== January 27 =====

//Title:// Listen!\\
//Reading material:// [[https://docs.oracle.com/javase/tutorial/uiswing/events/|The Java Tutorials: Writing Event Listeners]]\\
//Slides:// {{:public:lecture7.pdf|lecture7.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}}

===== January 30 =====

//Lab:// [[lab4|Lab 4]]

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

//Title:// Listen!\\
//Reading material:// Pages 27-29 of {{:public:notes.pdf|Notes}}, [[http://wuyongzheng.github.io/jpfdoc/gov/nasa/jpf/listener/package-summary.html|JPF API]]\\
//Slides:// {{:public:lecture8.pdf|lecture8.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)}}

===== February 3 =====

//Title:// Listen!\\
//Reading material:// Pages 30-32 of {{:public:notes.pdf|Notes}}\\
//Slides:// {{:public:lecture9.pdf|lecture9.pdf}}\\
//Code:// {{:public:statespace-3.txt|StateSpace.java (dot version with colours)}}, {{:public:mnemonics.txt|Mnemonics.java}}, {{:public:profiler.txt|Profiler.java}}\\
//Quiz:// [[quiz2|Quiz 2]]

===== February 6 =====

//Lab:// [[lab5|Lab 5]]

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

//Title:// Search!\\
//Reading material:// Chapter 8 of {{:public:notes.pdf|Notes}}\\
//Slides:// {{:public:lecture10.pdf|lecture10.pdf}}\\
//Code:// {{:public:DFSearch.txt|DFSearch.java}}

===== February 10 =====

//Title:// Search!\\
//Reading material:// Chapter 8 of {{:public:notes.pdf|Notes}}\\
//Slides:// {{:public:lecture11.pdf|lecture11.pdf}}\\
//Code:// {{:public:BFSearch.txt|BFSearch.java}}


===== February 13 =====

//Quiz:// [[quiz3|Quiz 3]]

===== February 15 =====

//Title:// Search!\\
//Reading material:// {{:public:randomsearch.txt|RandomSearch.java}}, {{:public:searchsample.txt|SearchSample.java}}\\
//Slides:// {{:public:lecture12.pdf|lecture12.pdf}}\\
//Code:// {{:public:randompathssearch.txt|RandomPathsSearch.java}}

===== February 17 =====

//Title:// The State Space in XML Format\\
//Reading material:// Section 8.6-8.8 and 11.1 of {{:public:notes.pdf|Notes}}\\
//Slides:// {{:public:lecture13.pdf|lecture13.pdf}}\\
//Code:// {{:public:statespacexml.txt|StateSpaceXML.java}}, {{:public:Sine.txt|Sine.java}}, {{:public:Sine-model.jpf.txt|Sine.jpf}}, {{:public:strictmath.txt|StrictMath.java}}

===== February 27 =====

//Lab:// [[lab7|Lab 7]]

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

//Title:// Handling Native Methods (Native Peers)\\
//Reading material:// Section 11.2 of {{:public:notes.pdf|Notes}}\\
//Slides:// {{:public:lecture14.pdf|lecture14.pdf}}\\
//Code:// {{:public:Sine.txt|Sine.java}}, {{:public:Sine.jpf.txt|Sine.jpf}}, {{:public:JPF_java_lang_StrictMath.txt|JPF_java_lang_StrictMath.java}}

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

//Title:// Concurrency\\
//Reading material:// [[https://docs.oracle.com/javase/tutorial/essential/concurrency/|The Java Tutorials: Concurrency]]\\
//Slides:// {{:public:lecture15.pdf|lecture15.pdf}}\\
//Code:// {{: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)}}

===== March 6 =====

//Lab:// [[lab8|Lab 8]]

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

//Title:// Concurrency\\
//Reading material:// [[https://docs.oracle.com/javase/tutorial/essential/concurrency/|The Java Tutorials: Concurrency]]\\
//Slides:// {{:public:lecture16.pdf|lecture16.pdf}}\\
//Code:// {{:public:Counter.txt|Counter.java}}, {{:public:Resource.txt|Resource.java}}

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

Last date to drop course without receiving grade

//Title:// Concurrency\\
//Reading material:// [[https://docs.oracle.com/javase/tutorial/essential/concurrency/|The Java Tutorials: Concurrency]]\\
//Slides:// {{:public:lecture17.pdf|lecture17.pdf}}\\
//Code:// {{:public:Database.txt|Database.java}}, {{:public:Reader.txt|Reader.java}}, {{:public:Writer.txt|Writer.java}}, {{:public:ReadersAndWriters.txt|ReadersAndWriters.java}}, {{:public:Table.txt|Table.java}}. {{:public:Philosopher.txt|Philosopher.java}}. {{:public:DiningPhilosophers.txt|DiningPhilosophers.java}}

===== March 13 =====

//Quiz:// [[Quiz4|Quiz 4]]

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

//Title:// Deadlocks and Data Races\\
//Reading material:// [[https://docs.oracle.com/javase/tutorial/essential/concurrency/|The Java Tutorials: Concurrency]]\\
//Slides:// {{:public:lecture18.pdf|lecture18.pdf}}\\
//Code:// {{:public:AbstractPhilosopher.txt|Philosopher.java}}, {{:public:LeftHandedPhilosopher.txt|LeftHandedPhilosopher.java}}, {{:public:RightHandedPhilosopher.txt|RightHandedPhilosopher.java}}, {{:public:LeftRightDiningPhilosophers.txt|DiningPhilosophers.java}}, {{:public:Room.txt|Room.java}}, {{:public:RoomPhilosopher.txt|Philosopher.java}}, {{:public:PhilosopherWithState.txt|Philosopher.java}}, {{:public:RaceAndCondition.txt|Account.java}}, {{:public:ConditionAndNoRace.txt|Account.java}}
, {{:public:RaceAndNoCondition.txt|Search.java}}


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

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

===== March 20 =====

//Lab:// [[lab10|Lab 10]]

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

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

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

//Title:// Computation Tree Logic\\
//Reading material:// pages 341-351 of the textbook\\
//Slides:// {{:public:lecture21.pdf|lecture21.pdf}}\\
//Course evaluation:// [[http://courseevaluations.yorku.ca|course evaluation]] at 10:05-10:15

===== March 27 =====

//Quiz:// [[quiz5|Quiz 5]]

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

//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:lecture22.pdf|lecture22.pdf}}

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

//Title:// Computation Tree Logic\\
//Reading material:// \\
//Slides:// {{:public:lecture23.pdf|lecture23.pdf}}

===== April 3 =====

Work on project

===== April 5 =====


//Title:// Model Checking versus Theorem Proving\\
//Slides:// {{:public:lecture24.pdf|lecture24.pdf}}\\
//Quiz:// [[quiz6|Quiz 6]]

Last day to withdraw from the course and receive a W (non-petitionable).

===== April 13 =====

Final exam in Accolade East, room 006, 9:00-11:00

===== April 16 =====

Deadline to hand in project

<html>
<!--














===== 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 22 =====

//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 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}}




-->
</html>