This is an old revision of the document!
Weekly Calendar
January 4
Title: Bugs are everywhere
Reading material: page 1-2, 4-6 of the textbook
Slides: lecture1.pdf
January 5
Title: Testing on steriods
Reading material: JUnit website
Slides: lecture2.pdf
January 7
Lab: Lab1
January 11
Title: Concurrency
Reading material: The Java Tutorials: Concurrency
Slides: lecture3.pdf
Code: Byte.java, ByteTest.java, Printer.java (using Thread), TwoPrinters.java (using Thread). Printer.java (using Runnable). TwoPrinters.java (using Runnable)
January 12
Title: States and transitions
Reading material: Section 2.3 of the textbook
Slides: lecture4.pdf
January 14
January 18
Title: Model Checking
Reading material: page 3, 7-10 of the textbook, The Java Tutorials: Concurrency
Slides: lecture5.pdf
Code: Counter.java, Resource.java
January 19
Title: Smaller Models
Reading material:
Slides: lecture6.pdf
Code: Semaphore.java, AtomicInteger.java
January 21
Reading material: The Java Tutorials: Concurrency
Lab: Lab3
January 25
Title: Introduction to Java PathFinder
Reading material: Java PathFinder: a translator from Java to Promela
Slides: lecture7.pdf
January 26
Title: Deadlocks and Race Conditions
Reading material: Section 3.1 of the textbook
Slides: lecture8.pdf
Code: Locker.java, TwoLockers.java, Friend.java, TwoFriends.java
January 28
Lab: Lab4
February 1
Title: Listeners
Reading material: The Java Tutorials: Writing Event Listeners
Slides: lecture9.pdf
Code: Generator.java, Listener.java, ListenerAdapter.java, Main.java, PlusPrinter.java, StarPrinter.java, SumPrinter.java, ValuePrinter.java
February 2
Title: Listeners in JPF
Reading material: Chapter 4 of Notes, JPF API
Slides: lecture10.pdf
Code: Garbage.java (prints *), Garbage.java (timer), StateSpace.java (txt version),StateSpace.java (dot version), StateSpace.java (dot version with colours)
February 4
Lab: Lab5
February 8
Title: Search Strategies in JPF
Reading material: Chapter 5 of Notes
Slides: lecture11.pdf
Code: 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
February 22
Title: Handling Native Methods (Model Classes)
Reading material:
Slides: lecture13.pdf
Code: Sine.java, StrictMath.java
February 23
Title: Handling Native Methods (Native Peers)
Reading material:
Slides: lecture14.pdf
Code: JPF_java_lang_StrictMath.java
February 25
Lab: Lab7
February 29
Title: The State Space in XML Format
Reading material:
Slides: lecture15.pdf
Code: StateSpacePrinter.java
March 1
Title: Linear Temporal Logic
Reading material: pages 229-236 of the textbook
Slides: lecture16.pdf
March 3
Lab: Lab8
March 7
Title: Linear Temporal Logic
Reading material: pages 237-249 of the textbook
Slides: lecture17.pdf
March 8
Title: Linear Temporal Logic
Reading material: pages 252, 255-256, 313-327, 334-340 of the textbook
Slides: 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 note on partial ordered sets and fixed points
Slides: lecture19.pdf
March 15
Title: Witnesses and Counterexamples
Reading material: pages 373-379 of the textbook
Slides: lecture20.pdf
March 17
Lab: work on your project and quiz on Computation Tree Logic