in conjunction with FSE 2012 , North Carolina
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.
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.
|8:45 AM||PF V7 (Intermediate)|
|8:45 AM||Intro To JPF, Install and Run JPF (Beginners)|
|10:15 AM||JPF V7 (Intermediate)|
|10:15 AM||Write a Listener (Beginners)|
|1:00 PM||Hacking Session (Write a listener in groups to check for Constraint Independence)|
|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 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
Peter Mehlitz, NASA Ames
Neha Rungta, NASA Ames
Willem Visser, U. Stellenbosch