Automatic handling of native methods in Java PathFinder

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.