Botha, Heila-MarieTkachuk, OVan der Merwe, BVisser, W2017-09-262017-09-262017-07Botha, H-M., Tkachuk, O., Van der Merwe, B. et al. 2017. Addressing challenges in obtaining high coverage when model checking android applications. Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software, 13-14 July 2017, Santa Barbara, California, USA, pp. 31-40978-1-4503-5077-8DOI: 10.1145/3092282.3092302http://scholar.google.com/citations?view_op=view_citation&hl=en&user=Ur1Pt7kAAAAJ&citation_for_view=Ur1Pt7kAAAAJ:IjCSPb-OGe4Chttp://spinroot.com/spin/symposia/ws17/SPIN_2017_paper_20.pdfhttp://dl.acm.org/citation.cfm?id=3092302http://hdl.handle.net/10204/9601Copyright: 2017 ACM. Due to copyright restrictions, the attached PDF file only contains the abstract of the full text item. For access to the full text item, kindly consult the publisher's website.Current dynamic analysis tools for Android applications do not get good code coverage since they can only explore a subset of the behaviors of the applications and do not have full control over the environment in which they execute. In this work we use model checking to systematically explore application paths while reducing the analysis size using state matching and backtracking. In particular, we extend the Java PathFinder (JPF) model checking environment for Android. We describe the difficulties one needs to overcome to make this a reality as well as our current approaches to handling these issues. We obtain significantly higher coverage using shorter event sequences on a representative sample of Android apps, when compared to Dynodroid and Sapienz, the current state-of-the-art dynamic analysis tools for Android applications.en-USAndroid applicationsConference PresentationBotha, H., Tkachuk, O., Van der Merwe, B., & Visser, W. (2017). Addressing challenges in obtaining high coverage when model checking android applications. ACM Digital Library. http://hdl.handle.net/10204/9601Botha, Heila-Marie, O Tkachuk, B Van der Merwe, and W Visser. "Addressing challenges in obtaining high coverage when model checking android applications." (2017): http://hdl.handle.net/10204/9601Botha H, Tkachuk O, Van der Merwe B, Visser W, Addressing challenges in obtaining high coverage when model checking android applications; ACM Digital Library; 2017. http://hdl.handle.net/10204/9601 .TY - Conference Presentation AU - Botha, Heila-Marie AU - Tkachuk, O AU - Van der Merwe, B AU - Visser, W AB - Current dynamic analysis tools for Android applications do not get good code coverage since they can only explore a subset of the behaviors of the applications and do not have full control over the environment in which they execute. In this work we use model checking to systematically explore application paths while reducing the analysis size using state matching and backtracking. In particular, we extend the Java PathFinder (JPF) model checking environment for Android. We describe the difficulties one needs to overcome to make this a reality as well as our current approaches to handling these issues. We obtain significantly higher coverage using shorter event sequences on a representative sample of Android apps, when compared to Dynodroid and Sapienz, the current state-of-the-art dynamic analysis tools for Android applications. DA - 2017-07 DB - ResearchSpace DP - CSIR KW - Android applications LK - https://researchspace.csir.co.za PY - 2017 SM - 978-1-4503-5077-8 T1 - Addressing challenges in obtaining high coverage when model checking android applications TI - Addressing challenges in obtaining high coverage when model checking android applications UR - http://hdl.handle.net/10204/9601 ER -