This is an old revision of the document!
Weekly Calendar
January 4
Title: Testing on steroids
Reading material: JUnit website
Slides: lab1.pdf
Lab: Lab 1
January 7
Title: Bugs are everywhere
Reading material: page 1-2, 4-6 of the textbook
Slides: lecture1.pdf
Handout: handout1.pdf
January 9
Title: Testing on steriods
Reading material: JUnit website
Slides: lecture2.pdf
Handout: handout2.pdf
Code: Color.java, ColorTest.java, BooleanTest.java
January 11
Quiz: Quiz 1
January 14
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
January 16
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, RunTest.java, RunTest.jpf
January 18
Lab: Lab 2
January 21
Quiz: Quiz 2, a solution
January 23
Title: Mini models
Slides: lecture5.pdf
Handout: handout5.pdf
Code: NoSoManyChoices.java, Choice.java
January 25
Reading material: Chapter 1 and 2 of notes.pdf
Project: Part 1 of project
Reading material: Chapter 4 of notes.pdf
Lab: Lab 3
January 28
Title: Mini models
Reading material: Chapter 3 of notes.pdf
Slides: lecture6.pdf
Handout: handout6.pdf
Code: RunJPF.java, Traversal.java
January 30
Title: Listen
Reading material: The Java Tutorials: Writing Event Listeners
Slides: lecture7.pdf
Handout: handout7.pdf
Code: Generator.java, Main.java, Listener.java, ListenerAdapter.java, PlusPrinter, StarPrinter.java, ValuePrinter.java, SumPrinter.java
February 1
February 4
Title: Listen
Reading material: Chapter 7 up to Section 7.4 of notes.pdf, new section for Chapter 7, JPF API
Slides: lecture8.pdf
Handout: handout8.pdf
Code: SearchEvents.java, StateSpace.java (txt version),StateSpace.java (dot version), StateSpace.java (dot version with colours)
February 6
Title: Listen
Reading material: The remainder of Chapter 7 of notes.pdf, JPF API
Slides: lecture9.pdf
Code: Garbage.java (first version), Garbage.java (second version), Example.java, Example.jpf, Mnemonics.java, Profiler.java
February 8
Lab: Lab 5
February 11
Title: Search
Reading material: Chapter 9, up to and including Section 9.6, of notes.pdf
Slides: lecture10.pdf
Handout: handout10.pdf
Code: DFSearch.java
February 13
Title: Search
Reading material: Section 9.7 of notes.pdf
Slides: lecture11.pdf
Handout: handout11.pdf
Code: BFSearch.java
February 15
Project: Part 2 of project
Quiz: Quiz 3
February 25
Title: Peers and Native Peers
Reading material: Chapter 10 of notes.pdf
Slides: lecture12.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
Project: Part 3 of project
February 27
March 1
Lab: Lab 6
March 4
Title: Testing JPF
Reading material: TestJPF
Slides: lecture13.pdf
Handout: handout13.pdf
Code: BasicTest.java, CallMonitorTest.java
March 6
Title: Concurrency
Reading material: The Java Tutorials: Concurrency
Slides: lecture14.pdf
Handout: handout14.pdf
Code: Printer.java (using Thread), TwoPrinters.java (using Thread). Printer.java (using Runnable). TwoPrinters.java (using Runnable), Incrementer.java, TwoIncrementers.java, TwoIncrementers.jpf
March 8
Drop deadline: last date to drop the course without receiving a grade for it.
Lab: work on your project
March 11
Title: Concurrency
Reading material: The Java Tutorials: Concurrency
Slides: lecture15.pdf, 
Handout: handout15.pdf
Code: Counter.java, Resource.java, StateSpaceWithThreadInfo.java
March 13
Title: Concurrency
Reading material: The Java Tutorials: Concurrency
Slides: lecture16.pdf
Handout: handout16.pdf
Code: Reader.java, Writer.java, ReadersAndWriters.java, Database.java (first attempt)
March 15
Lab: Lab 7
Project: Part 4 of project
March 18
Title: Concurrency
Reading material: The Java Tutorials: Concurrency
Slides: lecture17.pdf
Handout: handout17.pdf
Code: Database.java (second attempt), Philosopher.java,
Table.javaLeftHandedPhilosopher.java, RightHandedPhilosopher.java, DiningPhilosophers.java, Room.java, Philosopher.java, Philosopher.java
March 20
Title: Concurrency
Reading: The Java Tutorials: Concurrency
Slides: lecture18.pdf
Handout: handout18.pdf
Code: Account.java, Account.java
, Search.java
March 22
Lab: work on your project
March 25
Title: Linear Temporal Logic
Reading material: pages 229-236 and 248-249 of the textbook
Slides: lecture19.pdf
Handout: handout19.pdf
March 27
Title: Temporal Logics
Reading material: pages 313-327 and 334-340 of the textbook
Slides: lecture20.pdf
Handout: handout20.pdf
March 29
Lab: work on your project
Slides: lab12.pdf
Project: Part 5 of project
April 1
Title: CTL model checking
Reading material: pages 341-351 of the textbook
Slides: lecture21.pdf
April 3
Title: Symbolic model checking
Reading material:
Slides: lecture22.pdf
April 10
Final exam: 14:00-17:00 in LAS 1004.
April 22
<!--
===== March 15 =====
\\
//Recording:// [[recording|here (login with EECS credential to access this material)]]
===== March 29 =====
//Title:// Concurrency\\
//Reading//: [[https://docs.oracle.com/javase/tutorial/essential/concurrency/|The Java Tutorials: Concurrency]]\\
//Slides:// {{:lecture22.pdf|lecture22.pdf}}\\
//Handout:// {{:handout22.pdf|handout22.pdf}}\\
//Code:// {{:account.txt|Account.java}}, {{:customer.txt|Customer.java}}, {{:customers.txt|Customers.java}}, {{:account1.txt|Account.java}}\\
//Recording:// [[recording|here (login with EECS credential to access this material)]]\\
===== April 3 =====
//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:// {{:lecture23.pdf|lecture23.pdf}}\\
//Recording:// [[recording|here (login with EECS credential to access this material)]]
===== 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}}
-->