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

Slides (PDF) Download Slides (PDF)

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 slides

Lectures slides (PDF) Download Lectures slides (PDF)

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

Lecture slides (PDF) Download Lecture slides (PDF)