Java Pathfinder

This part consists of three lectures. Please watch the first three videos before Lecture 1, and two videos each before the other two lectures.

1. Introduction to concurrency and JPF

Watch

Software Model Checking (3:36)

 

Deadlock detection with JPF (3:39)

 

Shared conditions (5:50)

 

Read

Oracle's tutorial on concurrency Links to an external site.

Examples (source archives)

Examples with source (.tar.gz):

Use

tar -xvzf archive.tar.gz

to unpack the archives

Lecture slides and recording

Slides (PDF) Download Slides (PDF)

JPF and deadlocks (26:38)

 

JPF and shared conditions (46:50)

 

 

2. Data races and networked software with JPF

Watch

Data races (3:18)

 

Stubs in JPF (4:14)

 

Read

Runtime verification of networked software (tutorial paper)

Lecture recording and slides

Lectures slides (PDF) Download Lectures slides (PDF)

Data race analysis with JPF (30:46)

 

Analysis of networked software using stubs (37:00)

 

Tutorial and graded lab; jpf-nas (13:12)

 

 

Graded lab assignment

3. Networked software and JPF, Part 2

I/O caching in JPF (4:25)

 

Centralization (3:16)

 

Lecture slides and recording

Lecture slides (PDF) Download Lecture slides (PDF)

I/O caching (35:37)

 

Centralization (45:09)