{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,9]],"date-time":"2026-05-09T16:28:54Z","timestamp":1778344134780,"version":"3.51.4"},"reference-count":18,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2025,4,5]],"date-time":"2025-04-05T00:00:00Z","timestamp":1743811200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2025,6,30]]},"abstract":"<jats:p>The multitasking mechanism between activities and fragments plays a fundamental role in the Android operating system, which involves a wide range of features, including launch modes, intent flags, task affinities, and structured activities containing fragments. All of them are being widely used in Android apps, both open source and commercial ones. In this article, we present a formal semantics of the Android multitasking mechanism between activities and fragments, which accommodates all the important features and gives insofar the most comprehensive and accurate formalization. In particular, our semantics is formulated based on multi-stack systems, and fully captures the behavior of task stacks and activity stacks regarding fragments. Based on the semantics, we provide new static analysis algorithms, which are both multi-stack aware and fragment sensitive, thus achieve more precise static analysis for Android apps. We validate our approach by extensive experiments on both open source and commercial Android apps. The results highlight the benefits of the considering the semantics of the multitasking mechanism between activities and fragments in static analysis, and confirm the efficacy of our approach.<\/jats:p>","DOI":"10.1145\/3708562","type":"journal-article","created":{"date-parts":[[2024,12,18]],"date-time":"2024-12-18T10:50:41Z","timestamp":1734519041000},"page":"1-86","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Formalization of Android Activity-Fragment Multitasking Mechanism and Static Analysis of Mobile Apps"],"prefix":"10.1145","volume":"37","author":[{"ORCID":"https:\/\/orcid.org\/0009-0007-8145-4563","authenticated-orcid":false,"given":"Jinlong","family":"He","sequence":"first","affiliation":[{"name":"Key Laboratory of System Software (Chinese Academy of Sciences), Institute of Software Chinese Academy of Sciences, Beijing, China, State Key Laboratory of Computer Science, Institute of Software Chinese Academy of Sciences, Beijing, China, and School of Computer Science and Technology, University of Chinese Academy of Sciences, Beijing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0899-628X","authenticated-orcid":false,"given":"Zhilin","family":"Wu","sequence":"additional","affiliation":[{"name":"Key Laboratory of System Software (Chinese Academy of Sciences), Institute of Software Chinese Academy of Sciences, Beijing, China, State Key Laboratory of Computer Science, Institute of Software Chinese Academy of Sciences, Beijing, China, and School of Computer Science and Technology, University of Chinese Academy of Sciences, Beijing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5993-1665","authenticated-orcid":false,"given":"Taolue","family":"Chen","sequence":"additional","affiliation":[{"name":"School of Computing and Mathematical Sciences, Birkbeck, University of London, London, United Kingdom of Great Britain and Northern Ireland"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,4,5]]},"reference":[{"key":"e_1_3_3_2_2","unstructured":"Developers. 2023. Develop. Retrieved December 26 2024 from https:\/\/developer.android.com\/reference\/android\/content\/Intent#flags"},{"key":"e_1_3_3_3_2","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509549"},{"key":"e_1_3_3_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_22"},{"key":"e_1_3_3_5_2","doi-asserted-by":"publisher","unstructured":"Roberto Cavada Alessandro Cimatti Michele Dorigatti Alberto Griggio Alessandro Mariotti Andrea Micheli Sergio Mover Marco Roveri and Stefano Tonetta. 2014. The nuXmv symbolic model checker. In Computer Aided Verification. Lecture Notes in Computer Science Vol. 8559. Springer 334\u2013342. DOI:10.1007\/978-3-319-08867-9_22","DOI":"10.1007\/978-3-319-08867-9_22"},{"key":"e_1_3_3_6_2","doi-asserted-by":"publisher","DOI":"10.1109\/DSN.2018.00049"},{"key":"e_1_3_3_7_2","doi-asserted-by":"publisher","unstructured":"Taolue Chen Jinlong He Fu Song Guozhen Wang Zhilin Wu and Jun Yan. 2018. Android stack machine. In Computer Aided Verification. Lecture Notes in Computer Science Vol. 10982. Springer 487\u2013504. DOI:10.1007\/978-3-319-96142-2_29","DOI":"10.1007\/978-3-319-96142-2_29"},{"key":"e_1_3_3_8_2","doi-asserted-by":"crossref","unstructured":"Jinlong He Taolue Chen Ping Wang Zhilin Wu and Jun Yan. 2019. Android multitasking mechanism: Formal semantics and static analysis of apps. In Programming Languages and Systems. Lecture Notes in Computer Science Vol. 11893. Springer 291\u2013312.","DOI":"10.1007\/978-3-030-34175-6_15"},{"key":"e_1_3_3_9_2","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2017.8115638"},{"key":"e_1_3_3_10_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.infsof.2017.04.001"},{"key":"e_1_3_3_11_2","doi-asserted-by":"publisher","DOI":"10.1145\/3238147.3238188"},{"key":"e_1_3_3_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/2382196.2382223"},{"key":"e_1_3_3_13_2","doi-asserted-by":"publisher","unstructured":"Damien Octeau Daniel Luchaup Matthew L. Dering Somesh Jha and Patrick D. McDaniel. 2015. Composite constant propagation: Application to Android inter-component communication analysis. In Proceedings of the 37th IEEE\/ACM International Conference on Software Engineering (ICSE \u201915). IEEE 77\u201388. DOI:10.1109\/ICSE.2015.30","DOI":"10.1109\/ICSE.2015.30"},{"key":"e_1_3_3_14_2","volume-title":"Proceedings of the 22th USENIX Security Symposium","author":"Octeau Damien","year":"2013","unstructured":"Damien Octeau, Patrick D. McDaniel, Somesh Jha, Alexandre Bartel, Eric Bodden, Jacques Klein, and Yves Le Traon. 2013. Effective inter-component communication mapping in Android: An essential step towards holistic security analysis. In Proceedings of the 22th USENIX Security Symposium. 543\u2013558. https:\/\/www.usenix.org\/conference\/usenixsecurity13\/technical-sessions\/presentation\/octeau"},{"key":"e_1_3_3_15_2","first-page":"42","volume-title":"Proceedings of the 2017 IEEE International Conference on Software Quality, Reliability, and Security (QRS \u201917)","author":"Yan Jiwei","year":"2017","unstructured":"Jiwei Yan, Tianyong Wu, Jun Yan, and Jian Zhang. 2017. Widget-sensitive and back-stack-aware GUI exploration for testing Android apps. In Proceedings of the 2017 IEEE International Conference on Software Quality, Reliability, and Security (QRS \u201917). 42\u201353."},{"key":"e_1_3_3_16_2","doi-asserted-by":"publisher","DOI":"10.1145\/3551349.3560420"},{"key":"e_1_3_3_17_2","first-page":"105","volume-title":"Proceedings of the 44th 2022 IEEE\/ACM International Conference on Software Engineering: Companion Proceedings (ICSE Companion \u201922)","author":"Yan Jiwei","year":"2022","unstructured":"Jiwei Yan, Shixin Zhang, Yepang Liu, Jun Yan, and Jian Zhang. 2022. ICCBot: Fragment-aware and context-sensitive ICC resolution for Android applications. In Proceedings of the 44th 2022 IEEE\/ACM International Conference on Software Engineering: Companion Proceedings (ICSE Companion \u201922). IEEE, 105\u2013109."},{"key":"e_1_3_3_18_2","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2015.76"},{"key":"e_1_3_3_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/3180155.3180188"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3708562","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3708562","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T01:57:03Z","timestamp":1750298223000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3708562"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,4,5]]},"references-count":18,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2025,6,30]]}},"alternative-id":["10.1145\/3708562"],"URL":"https:\/\/doi.org\/10.1145\/3708562","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,4,5]]},"assertion":[{"value":"2024-04-02","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-12-02","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-04-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}