This section contains links to JPF presentations that might be of general interest. If you have slides, powerpoints, Keynote presentations or even just diagrams to share, please put them here with a short description of the content.

Here is the list of currently available presentations:

Generic 1-day JPF tutorial

This is a tutorial of about 85 slides that covers the following topics:

  1. introduction (45min)
  2. examples (2.5h, 16 demos)
  3. obtaining, building and running JPF (1h)
  4. JPF extension mechanisms (1.5h)

The first section is not very technical. The second one intends to show the whole spectrum of JPF applications, to do away with the prejudice of "JPF is just a model checker for concurrency bugs". There are currently slides for 16 motivating examples from jpf-core, jpf-awt, jpf-aprop, jpf-numeric, jpf-statechart, jpf-symbc and jpf-net-iocache. We will add more as they come. The third section is an abbreviated user guide, the fourth one gives an overview how you can extend JPF to fit your needs, covering the usual suspects like listeners, bytecode factories and native peers. This presentation will evolve over time, so check it out and give feedback.

The PDF slides are here. If you are a Keynote user, you get the presentation from here.

Symbolic PathFinder tutorial

Tutorial given by Willem Visser and Corina Pasareanu at ISSTA 2010.

  • Part 1 provides a generic introduction to Java Pathfinder, it core features, and configurations for use.
  • Part 2 provides an in-depth overview of Symbolic Pathfinder.

Trace Analysis and Server

The official title is about "Program Understanding & Defect Visualization", but what it really is about is trace analyzers (like DeadlockAnalyzer and MethodAnalyzer) and what has to be improved for them. This leads to the trace server, which is one of our GSoC 2010 projects.

The talk has four parts:

  1. introduction (10min)
  2. basics: model checking & listeners (10min)
  3. examples: oldclassic/DeadlockAnalyzer, RobotManager/MethodAnalyzer,OverlappingMethodAnalyzer (20min)
  4. outlook: trace server (5min)

The first two parts are just lifted from the generic tutorial. Part 3 uses the threaded RobotManager example from jpf-awt.

The PDF slides are here. If you are a Keynote user, you get the presentation from here.

jpf-mango slides for EclipseCon 2011

A port of mango to the Eclipse Workbench is underway. The hope is that the tool could be used in computer science classes, for example. But a LOT of work needs to happen, both in generating examples and extending functionality. My talk about this has been accepted for EclipseCon2011. Here is a link to the original slides. jpf-mango slides for EclipseCon 2011

The final version of the talk, transcript plus slides, stresses the actual implementation in the Eclipse workbench. EclipseCon 2011 slides and transcript

JPF talks and lab for Summer School on Formal Techniques 2011

This includes 3 1h lectures and a lab session about general JPF introduction for CS students, which were given at the First Summer School on Formal Techniques, 05/22 - 05/27/2011 at Menlo College, Atherton CA.

Especially the lab session is a good basis for hands-on tutorials of about 2h duration, but requires lectures 1 and 2 for the basics.

3 presentations related to symbolic execution and Symbolic PathFinder (given by Corina at ICSE'11 and ISSTA'11)

Combining Model Checking and Symbolic Execution for Software Testing

Automated Compositional Verification (Corina Pasareanu)

Lecture notes from Marktoberdorf Summer School (Corina Pasareanu)

Last modified 5 years ago Last modified on 01/24/2013 03:26:33 PM

Attachments (38)