Java PathFinder for Android Devices

Java PathFinder (JPF) has potential to be used for verification of Android apps, as they are written in Java. There is already an ongoing project to use JPF to verify Android apps outside of the Android platform, but such approach has limitations on the app functionality that can be verified, because modelling of Android environment on the desktop is difficult. Moreover, some apps cannot be properly analyzed in this way, as they rely on system events, make native calls, or interact with other Android apps that are unavailable outside the platform.

We propose an alternative approach: to create a fork of JPF and its extensions for Android platform. We plan to create an Android app that includes all sources of jpf-core, with necessary modifications, wrapped in the user interface (UI). The UI will start main method of underlying jpf-core, provide to it command line arguments, and display output. The underlying JPF will be executed as service.