Automated android.jar Generation With Binder/Interface Modeling for Android Services


Since Android uses Dalvik as a virtual machine, and because there are differences between Dalvik and standard Java virtual machines (JVMs), Java PathFinder (JPF) cannot model-check Android applications directly. The goal of this project is to create a tool for automatic generation of the Android Library (android.jar file in Android SDK) that will enable the model-checking of Android applications with JPF. The project will construct the library from Android sources and Android Interface Definition Language (AIDL) files which both use the Binder IPC for Android services. The project will further create models for the Binder IPC and native methods in the Android library. As such, the project bridges the gap between Dalvik and JPF in such a way it will be possible to model-check Android applications in JPF.


student: Marko Dimjašević <marko.dimjasevic AT>

mentor: Zvonimir Rakamaric

co-mentor: Eric Mercer


jpf-android-services is being hosted in


The project documentation is available at the jpf-android-services wiki.

Last modified 6 years ago Last modified on 06/04/2012 11:12:46 AM