NASA Logo, National Aeronautics and Space Administration
Intelligent Systems Division Banner

pocket knife

The Java Pathfinder Workshop 2012

November, 2012
in conjunction with FSE 2012 , North Carolina

Call for Participation

November 11, 2012: Java PathFinder Tutorial

The JPF tutorial will be targeted towards attendees who have never used JPF as well as researchers who use it as a development platform. The first part of the tutorial will present an introduction to JPF. It will provide an opportunity to the attendees to install JPF and analyze small examples using. The tutorial will present an overview of key features of JPF---configuration, listeners, and native peers. It will be followed by a description of its lesser known features such as the attribute system, interaction between listeners and execution engine, user extension of the state storage mechanism, and customized state matching. Some of these topics are targeted towards researchers who use JPF as a research platform for implementing various program analysis and model checking algorithms.

The second part of the tutorial will present an overview how various analysis extensions can be constructed on top of the JPF framework. Symbolic PathFinder (SPF) is the symbolic execution extension of JPF. We will present three different techniques that build upon SPF. The first is reliability analysis that allows one to calculate the probabilities of paths being executed. The second is a front-end that allows efficient constraint solving by providing a mechanism to reuse previously calculated results. Finally, the third technique leverages SPF to compute the impact of changes between two related programs.

November 12: Presentations on Accepted Papers

  • Symbolic Quantitative Information Flow, Quoc-Sang Phan, Pasquale Malacaria, Oksana Tkachuk and Corina S. Pasareanu
  • S2PF: Speculative Symbolic PathFinder, Yufeng Zhang, Zhenbang Chen and Ji Wang
  • An Extension of JavaPath Finder for Hybrid Systems, Laura Panizo and Maria Del Mar Gallardo
  • Abstract Pathfinder, Artem Khyzha, Pavel Parizek and Corina Pasareanu
  • Test Generation Via Symbolic Simulation, Frank Rimlinger
  • Tools to Generate and Check Consistency of Model Classes for Java PathFinder, Matteo Ceccarello and Nastaran Shafiei
  • Verifying Android Applications using Java PathFinder, Heila van der Merwe, Willem Visser and Brink van der Merwe
  • Testing Android Apps Through Symbolic Execution, Nariman Mirzaei, Sam Malek, Corina Pasareanu, Naeem Esfahani and Riyadh Mahmood
  • Ranged Model Checking, Diego Funes, Sarfraz Khurshid and Junaid Haroon Siddiqui
  • Modeling Class loaders in Java PathFinder Version 7, Nastaran Shafiei and Peter Mehlitz
  • Computing and Visualizing the Impact of Change with Java PathFinder Extensions, Eric Mercer, Suzette Person and Neha Rungta


    Registration for the JPF Workshop will be through the registration page of FSE 2012 .

    Social Event

    There will be a dinner for JPF Workshop attendees on November 11th at 6:30 PM.

    Call for Contributions

    We solicit submissions for existing research, applications, work in progress, and position papers on topics related to JPF or its extensions. If the underlying research idea has been published in another venue the paper needs to clarify the novel aspects that are being presented in the paper. We also solicit comparative analysis papers that evaluate algorithms in JPF or its extensions with relevant tools. The goal of the workshop is to encourage the flow of ideas relevant to JPF. The papers should be at most 5 pages long in the ACM Proceedings format.
    Accepted papers will be published in the ACM digital library.

    Important Dates

    • Abstract Submission Deadline: July 24, 2012
    • Full Paper Submission Deadline: Aug 1, 2012
    • Notification of Acceptance: Aug 15, 2012
    • Final Version Submission: Sept 2, 2012


    Nov 11th
    8:45 AMPF V7 (Intermediate)
    8:45 AMIntro To JPF, Install and Run JPF (Beginners)
    9:45 AMBreak
    10:15 AM JPF V7 (Intermediate)
    10:15 AM Write a Listener (Beginners)
    12:00 PM Lunch
    1:00 PM Hacking Session (Write a listener in groups to check for Constraint Independence)
    2:00 PM Break
    2:30 PM Green with Symbolic Execution
    3:30 PM Directed Incremental Symbolic Execution
    4:00 PM Probilistic Symbolic Execution
    4:30 PM Wrap up (Questions)
    Meet in the lobby of embassay suites to go to dinner at Biaggis'
    Nov 12th
    09:00 AM Welcome
    09:05 AM S2PF: Speculative Symbolic PathFinder
    09:25AM Testing Android Apps Through Symbolic Execution
    09:45AM Break
    10:30 AM Test Generation Via Symbolic Simulation
    10:50 AM Computing and Visualizing the Impact of Change with Java PathFinder Extensions
    11:10 AM Abstract PathFinder
    11:30 AM Symbolic Quantitative Information Flow
    11:50 AM Lunch
    1:00 PM An extension of Java PathFinder for Hybrid Systems
    1:20 PM Ranged Model Checking
    1:40 PM Verifying Android Applications using Java PathFinder
    2:00 PMTools to Generate and Check Consistency for Model Classes for Java PathFinder
    2:20 PM Modeling class loaders in Java Pathfinder Version 7
    2:40 PM Break
    3:15:5:00 How to do ____ in JPF session and other discussion


Program Chairs:
Peter Mehlitz, NASA Ames
Neha Rungta, NASA Ames
Willem Visser, U. Stellenbosch

Program Committee
Cyrille Artho
Marcelo D'Amorim
Indradeep Ghosh
Dimitra Giannakopulou
Alex Groce
Klaus Havelund
Sarfraz Khurshid
Darko Marinov
Steve Lauterburg
Eric Mercer
Suzette Person
Zvonimir Rakamaric
Franco Raimondi
Frank Rimlinger
Oksana Tkachuk

First Gov logo
NASA Logo -