2014 International SPIN Symposium on Model Checking of Software (SPIN), July 21–23, 2014, San Jose, CA, USA

Desktop Layout

Model Checking II
Santa Clara Room, Chair: Stefan Leue
Automatic Handling of Native Methods in Java PathFinder
Publisher's Version
Abstract: Java PathFinder (JPF) is a model checker for Java applications. Despite its maturity, JPF cannot be used to verify any realistic Java application without a nontrivial amount of work done by its user. One of the main limiting factors towards model checking such applications is handling native calls. JPF provides ways for users to handle such calls. However, those require modeling the behaviour of the native methods in Java which is labour intensive and hinders the uptake of JPF by developers. This paper presents our tool that extends JPF to address this problem. Our work alleviates this burden for users by automatically handling native calls. Our approach is based on delegating the execution of native calls from JPF to their original execution environment. We showcase our extension by applying it to a variety of simple yet realistic Java applications that JPF, without our extension, cannot handle.

Time stamp: 2020-07-13T11:22:50+02:00