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

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

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

Quiz: Quiz 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, RunTest.java, RunTest.jpf

Lab: Lab 2

Quiz: Quiz 2, a solution

Title: Mini models
Slides: lecture5.pdf
Handout: handout5.pdf
Code: NoSoManyChoices.java, Choice.java

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

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

Title: Mini models
Reading material: Chapter 3 of notes.pdf
Slides: lecture6.pdf
Handout: handout6.pdf
Code: RunJPF.java, Traversal.java

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

Reading material: Chapter 7 of notes.pdf, JPF API
Lab: Lab 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)

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

Lab: Lab 5

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

Title: Search
Reading material: Section 9.7 of notes.pdf
Slides: lecture11.pdf
Handout: handout11.pdf
Code: BFSearch.java

Project: Part 2 of project
Quiz: Quiz 3

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

Midterm, a solution

Lab: Lab 6

Title: Testing JPF
Reading material: TestJPF
Slides: lecture13.pdf
Handout: handout13.pdf
Code: BasicTest.java, CallMonitorTest.java

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

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

Lab: work on your project

Title: Concurrency
Reading material: The Java Tutorials: Concurrency
Slides: lecture15.pdf,
Handout: handout15.pdf
Code: Counter.java, Resource.java, StateSpaceWithThreadInfo.java

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)

Lab: Lab 7

Project: Part 4 of project

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

Title: Concurrency
Reading: The Java Tutorials: Concurrency
Slides: lecture18.pdf
Handout: handout18.pdf
Code: Account.java, Account.java , Search.java

Lab: work on your project

Title: Linear Temporal Logic
Reading material: pages 229-236 and 248-249 of the textbook
Slides: lecture19.pdf
Handout: handout19.pdf

Title: Temporal Logics
Reading material: pages 313-327 and 334-340 of the textbook
Slides: lecture20.pdf
Handout: handout20.pdf

Lab: work on your project
Slides: lab12.pdf

Project: Part 5 of project

Title: CTL model checking
Reading material: pages 341-351 of the textbook
Slides: lecture21.pdf

Title: Symbolic model checking
Reading material: Combining unit-level symbolic execution and system-level concrete execution for testing NASA software
Slides: lecture22.pdf

Office hours: 14:00-16:00

Office hours: 10:00-12:00

Final exam, a solution: 14:00-17:00 in LAS 1004.

Project

<!--   ===== 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}}   -->