The Java Pathfinder Workshop 2012

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

  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

  Schedule

  Nov 11th
  8:45 AM	PF V7 (Intermediate)
  8:45 AM	Intro To JPF, Install and Run JPF (Beginners)
  9:45 AM	Break
  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)
  6:00	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 PM	Tools 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