{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T14:59:42Z","timestamp":1761663582422,"version":"3.37.3"},"reference-count":75,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"6","license":[{"start":{"date-parts":[[2018,6,1]],"date-time":"2018-06-01T00:00:00Z","timestamp":1527811200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"}],"funder":[{"name":"Singapore NRF","award":["RGNRF1501"],"award-info":[{"award-number":["RGNRF1501"]}]},{"name":"NRF","award":["88210"],"award-info":[{"award-number":["88210"]}]},{"DOI":"10.13039\/501100001381","name":"National Research Foundation, Prime Ministers Office, Singapore","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100001381","id-type":"DOI","asserted-by":"crossref"}]},{"name":"National Cybersecurity R&D Program","award":["NRF2014NCR-NCR001-30"],"award-info":[{"award-number":["NRF2014NCR-NCR001-30"]}]},{"name":"National Cybersecurity R&D Directorate"},{"name":"National University of Singapore and Singapore University of Technology and Design"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IIEEE Trans. Software Eng."],"published-print":{"date-parts":[[2018,6,1]]},"DOI":"10.1109\/tse.2017.2697848","type":"journal-article","created":{"date-parts":[[2017,4,25]],"date-time":"2017-04-25T18:41:53Z","timestamp":1493145713000},"page":"595-612","source":"Crossref","is-referenced-by-count":23,"title":["Towards Model Checking Android Applications"],"prefix":"10.1109","volume":"44","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6390-9890","authenticated-orcid":false,"given":"Guangdong","family":"Bai","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Quanqi","family":"Ye","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yongzheng","family":"Wu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Heila","family":"Botha","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jun","family":"Sun","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yang","family":"Liu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jin Song","family":"Dong","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Willem","family":"Visser","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref73","first-page":"250","article-title":"A grey-box\n approach for automated GUI-model generation of mobile applications","author":"yang","year":"2013","journal-title":"Proc 16th Int Conf Fundam Approaches Softw Eng"},{"key":"ref72","doi-asserted-by":"publisher","DOI":"10.1145\/2381934.2381950"},{"key":"ref71","doi-asserted-by":"crossref","DOI":"10.14722\/ndss.2016.23066","article-title":"Harvesting runtime values\n in Android applications that feature anti-analysis techniques","author":"rasthofer","year":"2016","journal-title":"Proc Symp Network and Distributed System Security"},{"key":"ref70","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/2382756.2382798","article-title":"Testing Android apps through symbolic execution","volume":"37","author":"mirzaei","year":"2012","journal-title":"SIGSOFT Softw Eng Notes"},{"key":"ref74","first-page":"623","article-title":"Guided GUI\n testing of Android apps with minimal restart and approximate learning","author":"choi","year":"2013","journal-title":"Proc ACM SIGPLAN Int Conf Object Oriented Program Syst Languages Appl"},{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2010.26"},{"key":"ref75","doi-asserted-by":"publisher","DOI":"10.1145\/2491411.2491450"},{"key":"ref38","first-page":"543","article-title":"Effective inter-component communication\n mapping in Android: An essential step towards holistic security analysis","author":"octeau","year":"2013","journal-title":"Proc 22nd USENIX Secur Symp"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1023\/A:1026599015809"},{"key":"ref32","first-page":"121","article-title":"A survey of program slicing techniques","volume":"3","author":"tip","year":"1995","journal-title":"J Program Languages"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1984.5010248"},{"key":"ref30","first-page":"393","article-title":"TaintDroid: An information-flow tracking\n system for realtime privacy monitoring on smartphones","author":"enck","year":"2010","journal-title":"Proc 9th USENIX Conf Operating Syst Des Implementation"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2014.23039"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1145\/2480362.2480706"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1145\/2382196.2382222"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1145\/2046707.2046779"},{"key":"ref60","doi-asserted-by":"publisher","DOI":"10.1109\/ICECCS.2015.20"},{"key":"ref62","article-title":"Contextual policy enforcement in Android\n applications with permission event graphs","author":"chen","year":"2013","journal-title":"Proc 20th Annu Netw Distrib Syst Security Symp"},{"key":"ref61","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/2557833.2560576","article-title":"Execution and property specifications for JPF-Android","volume":"39","author":"van der merwe","year":"2014","journal-title":"ACM SIGSOFT Softw Eng Notes"},{"key":"ref63","doi-asserted-by":"publisher","DOI":"10.1145\/2568225.2568301"},{"year":"0","key":"ref28","article-title":"CVE"},{"key":"ref64","doi-asserted-by":"publisher","DOI":"10.1109\/GLOCOM.2015.7417621"},{"article-title":"Obfuscating embedded malware on android","year":"0","author":"ionescu","key":"ref27"},{"key":"ref65","doi-asserted-by":"publisher","DOI":"10.1109\/ICECCS.2015.17"},{"key":"ref66","first-page":"280","article-title":"IccTA: detecting inter-component privacy leaks in Android apps","author":"li","year":"2015","journal-title":"Proceedings of the International Conference on Software Engineering ICSE'94"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1145\/2660267.2660343"},{"key":"ref67","doi-asserted-by":"publisher","DOI":"10.1145\/379605.379665"},{"key":"ref68","doi-asserted-by":"publisher","DOI":"10.1145\/2508859.2516689"},{"key":"ref69","first-page":"29","article-title":"DroidScope: Seamlessly reconstructing the OS and Dalvik semantic views for dynamic Android\n malware analysis","author":"yan","year":"2012","journal-title":"Proc 21st USENIX Conf Security Symp"},{"year":"0","key":"ref2","article-title":"Number of available Android applications"},{"year":"0","key":"ref1","article-title":"Smartphone OS market share, 2016 Q3"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1145\/2557833.2560572"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2011.6100131"},{"key":"ref21","first-page":"1","article-title":"Generation of library\n models for verification of Android applications","author":"van der merwe","year":"2014","journal-title":"Proc Java Pathfinder Workshop"},{"key":"ref24","first-page":"209","article-title":"KLEE:\n Unassisted and automatic generation of high-coverage tests for complex systems programs","author":"cadar","year":"2008","journal-title":"Proc 8th USENIX Conf Operating Syst Des Implementation"},{"key":"ref23","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/2382756.2382797","article-title":"Verifying Android applications using Java PathFinder","volume":"37","author":"van der merwe","year":"2012","journal-title":"ACM SIGSOFT Softw Eng Notes"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1145\/2484313.2484355"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1145\/1950365.1950396"},{"key":"ref50","doi-asserted-by":"publisher","DOI":"10.1145\/2393596.2393666"},{"key":"ref51","doi-asserted-by":"publisher","DOI":"10.1145\/2508859.2516676"},{"key":"ref59","first-page":"110","article-title":"Trustfound:\n Towards a formal foundation for model checking trusted computing platforms","author":"bai","year":"2014","journal-title":"Proc 19th Int Symp Formal Methods"},{"key":"ref58","first-page":"1","article-title":"Model checking LTL properties over\n ANSI-C programs with bounded traces","volume":"14","author":"morse","year":"2013","journal-title":"Softw Syst Model"},{"key":"ref57","doi-asserted-by":"publisher","DOI":"10.1145\/1189256.1189259"},{"key":"ref56","doi-asserted-by":"publisher","DOI":"10.1145\/2043556.2043582"},{"key":"ref55","doi-asserted-by":"crossref","first-page":"110","DOI":"10.1145\/1040305.1040315","article-title":"Dynamic partial-order reduction for model checking software","author":"flanagan","year":"2005","journal-title":"Proceedings of the ACM SIGACT-SIGPLAN Symp Principles of Programming Languages"},{"key":"ref54","doi-asserted-by":"publisher","DOI":"10.1145\/1858996.1859035"},{"key":"ref53","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2011.6100119"},{"key":"ref52","doi-asserted-by":"publisher","DOI":"10.1145\/1985793.1985995"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594299"},{"key":"ref11","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1007\/978-3-642-30921-2_17","article-title":"AndroidLeaks: Automatically detecting\n potential privacy leaks in Android applications on a large scale","author":"gibler","year":"2012","journal-title":"Proc International Conference on Trust and Trustworthy Computing"},{"year":"0","key":"ref40","article-title":"Process lifecycle"},{"article-title":"SCanDroid: Automated security certification of Android applications","year":"2009","author":"fuchs","key":"ref12"},{"key":"ref13","article-title":"Systematic detection of capability leaks\n in stock Android smartphones","author":"grace","year":"2012","journal-title":"Proc 19th Annu Netw Distrib Syst Security Symp"},{"year":"0","key":"ref14","article-title":"Open source 360"},{"key":"ref15","first-page":"641","article-title":"Targeted and depth-first exploration for systematic testing of Android apps","author":"azim","year":"2013","journal-title":"Proc ACM SIGPLAN Int Conf Object Oriented Program Syst Languages Appl"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1145\/2594368.2594390"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1023\/A:1022920129859"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378846"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2003.1240300"},{"key":"ref4","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1007\/978-3-642-21599-5_7","article-title":"Taming information-stealing smartphone\n applications (on Android)","author":"zhou","year":"2011","journal-title":"Proc 4th Int Conf on Trust and Trustworthy Computing"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2012.16"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1145\/2382196.2382223"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1145\/2185448.2185464"},{"key":"ref8","article-title":"Towards taming privilege-escalation attacks on Android","author":"bugiel","year":"2012","journal-title":"Proc 19th Annu Netw Distrib Syst Security Symp"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1145\/2414456.2414498"},{"key":"ref49","article-title":"DTA++: Dynamic taint analysis with\n targeted control-flow propagation","author":"kang","year":"2011","journal-title":"Proc 18th Annu Netw Distrib Syst Secur Symp"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1145\/2435349.2435379"},{"key":"ref46","article-title":"AdSplit: Separating smartphone advertising from applications","author":"shekhar","year":"2012","journal-title":"Proc 21st USENIX Conf Security Symp"},{"year":"0","key":"ref45","article-title":"Insecurebank"},{"key":"ref48","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384623"},{"key":"ref47","doi-asserted-by":"publisher","DOI":"10.1109\/ICECCS.2014.13"},{"year":"0","key":"ref42","article-title":"dex2jar"},{"year":"0","key":"ref41","article-title":"apktool"},{"year":"0","key":"ref44","article-title":"GPS share"},{"key":"ref43","doi-asserted-by":"publisher","DOI":"10.1145\/2393596.2393600"}],"container-title":["IEEE Transactions on Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/32\/8383624\/07911333.pdf?arnumber=7911333","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,26]],"date-time":"2022-01-26T03:04:07Z","timestamp":1643166247000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/7911333\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,6,1]]},"references-count":75,"journal-issue":{"issue":"6"},"URL":"https:\/\/doi.org\/10.1109\/tse.2017.2697848","relation":{},"ISSN":["0098-5589","1939-3520"],"issn-type":[{"type":"print","value":"0098-5589"},{"type":"electronic","value":"1939-3520"}],"subject":[],"published":{"date-parts":[[2018,6,1]]}}}