Title: Bugs are everywhere
Reading material: page 1-2, 4-6 of the textbook
Slides: lecture1.pdf

Title: Testing on steriods
Reading material: JUnit website
Slides: lecture2.pdf
Handout: handout1.pdf, handout2.pdf
Code: ColorTest.java

Title: More testing on steroids
Reading material: JUnit website
Slides: lab1.pdf
Lab: Lab 1

Title: Space exploration
Reading material: page 3, 7-8, 11-16 of the textbook
Slides: lecture3.pdf
Handout: handout3.pdf
Code: OneChoice.java, TwoChoices.java, ManyChoices.java, ManyChoices.java

Title: Check models
Reading material: Section 1 and Section 5.1-5.3 of The Birth of Model Checking, Java PathFinder: a translator from Java to Promela
Slides: lecture4.pdf
Handout: handout4.pdf
Code: PrintRandom.java, PrintRandom.jpf

Quiz: Quiz 1

Title: State space traversals
Reading material: Chapter 5 of notes.pdf
Slides: lecture5.pdf
Handout: handout5.pdf
Code: RunTest.java, RunTest.jpf, RunJPF.java, Traversal.java

Title: Listen
Reading material: The Java Tutorials: Writing Event Listeners
Slides: lecture6.pdf
Handout: handout6.pdf
Code: Generator.java, Main.java, Listener.java, ListenerAdapter.java, PlusPrinter, StarPrinter.java, ValuePrinter.java, SumPrinter.java

Reading material: Chapter 1 and 2 of notes.pdf
Project: Part 1 of project

Reading material: Chapter 5 of notes.pdf
Lab: Lab 2

Title: Listen
Reading material: Chapter 7 up to Section 7.5 of notes.pdf, JPF API
Slides: lecture7.pdf
Handout: handout7.pdf
Code: SearchEvents.java, Traversal.java, Traversal.jpf, StateSpaceText.java, Traversal.jpf, StateSpaceDot.java, StateSpaceDot.java (version with colours)

Title: Listen
Reading material: The remainder of Chapter 7 of notes.pdf, JPF API
Slides: lecture8.pdf
Code: Garbage.java (first version), Garbage.java (second version), GarbageTest.java, GarbageTest.jpf, Mnemonics.java, Profiler.java

Quiz: Quiz 2

Title: Search
Reading material: Chapter 9, up to and including Section 9.6, of notes.pdf
Slides: lecture9.pdf
Handout: handout9.pdf
Code: DFSearch.java

Title: Search
Reading material: the remainder of Chapter 9 of notes.pdf
Slides: lecture10.pdf
Handout: handout10.pdf
Code: BFSearch.java, Generate.java, Sample.java (generated app), SearchNotificationRecorder, CompareSearchRecordings, test.sh

Reading material: Chapter 9 of notes.pdf
Lab: Lab 3

Title: Linear Temporal Logic
Reading material: pages 229-236 of the textbook
Slides: lecture11.pdf
Handout: handout11.pdf

Title: Temporal Logics
Reading material: pages 174-175, 248-249, 271-272, 313-327 and 334-340 of the textbook
Slides: lecture12.pdf
Handout: handout12.pdf

Quiz: Quiz 3
Project: Part 2 of project

Project: Part 3 of project

Title: Computational Tree Logic
Reading material: pages 341-351 of the textbook
Slides: lecture13.pdf
Handout: handout13df

Title: Testing JPF
Reading material: notes on testing JPF components,TestJPF
Slides: lecture14.pdf
Handout: handout14.pdf
Code: BasicTest.java, CallMonitorTest.java

Lab: Lab 4

Midterm a solution

Title: Peers and Native Peers
Reading material: Chapter 10 of notes.pdf
Slides: lecture15.pdf
Handout: handout15.pdf
Code: TeleTYpewriter.java, Main.java, my_util_TeleTypewriter.h, my_util-TeleTYpewriter.c, TeleTYpewriter.java (peer class), Main.jpf (using peer class), JPF_my_util_TeleTYpewriter.java (native peer class), Main.jpf (using native peer class), Main.jpf (using jpf-nhandler

Lab: Lab 5

Project: Part 4 of project

Title: Concurrency
Reading material: The Java Tutorials: Concurrency
Slides: lecture16.pdf
Handout: handout16.pdf
Code: Printer.java (using Thread), TwoPrinters.java (using Thread). Printer.java (using Runnable). TwoPrinters.java (using Runnable), TwoPrinters.java (using anonymous class)Incrementer.java, TwoIncrementers.java, TwoIncrementers.jpf

Title: Concurrency
Reading material: The Java Tutorials: Concurrency
Slides: lecture17.pdf
Handout: handout17.pdf
Code: Counter.java, Resource.java, User.java, MultipleUsers.java

Lab: Lab 6

Title: Concurrency
Reading material: The Java Tutorials: Concurrency, Section 3.1 of the textbook
Slides: lecture18.pdf
Handout: handout18.pdf
Code: Reader.java, Writer.java, ReadersAndWriters.java, Database.java, Philosopher.java, Table.java, DiningPhilosophers.java
Recording: recording

Title: Concurrency
Reading material: The Java Tutorials: Concurrency
Slides: lecture19.pdf
Code: Scheduling.java, Philosopher.java, Table.javaLeftHandedPhilosopher.java, RightHandedPhilosopher.java, DiningPhilosophers.java (left and right handed), Philosopher.java, Table.java, DiningPhilosophers.java (philosophers sits down before picking of the forks), Philosopher.java, DiningPhilosophers.java (states)
Recording: recording

Lab: Lab 7

Project: Part 5 of project

Title: Undecidability
Slides: lecture20.pdf
Recording: recording

Title: Data races
Slides: lecture21.pdf
Handout: handout21.pdf
Code: Code: Account.java, Account.java, Search.java
Recording: recording

Lab: Lab 8

Slides of sample presentation Recording of sample presentation

Presentation schedule:

1. Rajvi Chavada and Connor Dear
2. Syed Usman
3. Connor Ahearn and Jeremy Winkler
4. Damanveer Bharaj
5. Sara Attalla and Sean Doyle

Recording: recording

Presentations

1. Gagen Benipal and Zaeem Israr
2. Kevin Banh and Andrew Maywapersaud
3. Anji Tong
4. Aya Abu Allan and Mark Savin
5. Dong Jae Lee
6. Bradley Booth and Akbar Khan

Recording: recording

Lab: Lab 9

Final exam at 7pm

Project: final report and code

Drop deadline: last date to drop the course without receiving a grade for it.

Updates from York University Senate

<!--   ===== January 23 =====   //Title:// Mini models\\ //Slides:// {{:lecture5.pdf|lecture5.pdf}}\\ //Handout:// {{:handout5.pdf|handout5.pdf}}\\ //Code:// {{:nosomanychoices.txt|NoSoManyChoices.java}}, {{:choice.txt|Choice.java}}   {{:statespacewithouthtreadinfo.png?200x50|state space diagram}}\\   //Code:// {{:statespacewiththreadinfo.txt|StateSpaceWithThreadInfo.java}}     ===== March 18 =====   //Title:// Concurrency\\ //Reading material:// [[https://docs.oracle.com/javase/tutorial/essential/concurrency/|The Java Tutorials: Concurrency]]\\ //Slides:// {{:lecture17.pdf|lecture17.pdf}}\\ //Handout:// {{:handout17.pdf|handout17.pdf}}\\ //Code:// {{:public:AbstractPhilosopher.txt|Philosopher.java}}, {{:public:table.txt|Table.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}}   ===== March 20 =====   //Title:// Concurrency\\ //Reading//: [[https://docs.oracle.com/javase/tutorial/essential/concurrency/|The Java Tutorials: Concurrency]]\\ //Slides:// {{:lecture18.pdf|lecture18.pdf}}\\ //Handout:// {{:handout18.pdf|handout18.pdf}}\\ //Code:// {{:public:RaceAndCondition.txt|Account.java}}, {{:public:ConditionAndNoRace.txt|Account.java}} , {{:public:RaceAndNoCondition.txt|Search.java}}   ===== March 22 =====   //Lab:// work on your project   ===== March 29 =====   //Lab:// work on your project\\ //Slides:// {{:lab12.pdf|lab12.pdf}}   //Project:// [[project5|Part 5 of project]]   ===== April 3 =====   //Title:// Symbolic model checking\\ //Reading material:// [[http://dx.doi.org.ezproxy.library.yorku.ca/10.1145/1390630.1390635|Combining unit-level symbolic execution and system-level concrete execution for testing NASA software]]\\ //Slides:// {{:lecture22.pdf|lecture22.pdf}}   ===== April 8 =====   //Office hours:// 14:00-16:00   ===== April 9 =====   //Office hours:// 10:00-12:00   ===== April 10 =====   [[final|Final exam]], {{:final.pdf|a solution}}: 14:00-17:00 in LAS 1004.   ===== April 22 =====   [[project6|Project]]   -->