{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,22]],"date-time":"2025-06-22T21:40:01Z","timestamp":1750628401516,"version":"3.41.0"},"publisher-location":"Cham","reference-count":20,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319624068"},{"type":"electronic","value":"9783319624075"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-62407-5_15","type":"book-chapter","created":{"date-parts":[[2017,7,14]],"date-time":"2017-07-14T11:16:58Z","timestamp":1500031018000},"page":"218-232","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Separation Logic for States Dependencies in Life Cycles of Android Activities and Fragments"],"prefix":"10.1007","author":[{"given":"Mohamed A.","family":"El-Zawawy","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,7,15]]},"reference":[{"key":"15_CR1","unstructured":"Android developers. http:\/\/developer.android.com"},{"issue":"6","key":"15_CR2","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1145\/2666356.2594299","volume":"49","author":"S Arzt","year":"2014","unstructured":"Arzt, S., Rasthofer, S., Fritz, C., Bodden, E., Bartel, A., Klein, J., Le Traon, Y., Octeau, D., McDaniel, P.: Flowdroid: precise context, flow, field, object-sensitive and lifecycle-aware taint analysis for android apps. ACM Sigplan Not. 49(6), 259\u2013269 (2014)","journal-title":"ACM Sigplan Not."},{"key":"15_CR3","doi-asserted-by":"crossref","unstructured":"Barrera, D., Kayacik, H.G., van Oorschot, P.C., Somayaji, A.: A methodology for empirical analysis of permission-based security models and its application to android. In: Proceedings of the 17th ACM Conference on Computer and Communications Security, pp. 73\u201384. ACM (2010)","DOI":"10.1145\/1866307.1866317"},{"key":"15_CR4","doi-asserted-by":"crossref","unstructured":"Bartel, A., Klein, J., Le Traon, Y., Monperrus, M.: Dexpler: converting android dalvik bytecode to jimple for static analysis with soot. In: Proceedings of the ACM SIGPLAN International Workshop on State of the Art in Java Program Analysis, pp. 27\u201338. ACM (2012)","DOI":"10.1145\/2259051.2259056"},{"key":"15_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"100","DOI":"10.1007\/978-3-319-42092-9_9","volume-title":"Computational Science and Its Applications \u2013 ICCSA 2016","author":"MA El-Zawawy","year":"2016","unstructured":"El-Zawawy, M.A.: An operational semantics for android applications. In: Gervasi, O., et al. (eds.) ICCSA 2016. LNCS, vol. 9790, pp. 100\u2013114. Springer, Cham (2016). doi:10.1007\/978-3-319-42092-9_9"},{"key":"15_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/978-3-319-42092-9_10","volume-title":"Computational Science and Its Applications \u2013 ICCSA 2016","author":"MA El-Zawawy","year":"2016","unstructured":"El-Zawawy, M.A.: A type system for android applications. In: Gervasi, O., et al. (eds.) ICCSA 2016. LNCS, vol. 9790, pp. 115\u2013128. Springer, Cham (2016). doi:10.1007\/978-3-319-42092-9_10"},{"issue":"2","key":"15_CR7","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1145\/2619091","volume":"32","author":"W Enck","year":"2014","unstructured":"Enck, W., Gilbert, P., Han, S., Tendulkar, V., Chun, B.-G., Cox, L.P., Jung, J., McDaniel, P., Sheth, A.N.: Taintdroid: an information-flow tracking system for realtime privacy monitoring on smartphones. ACM Trans. Comput. Syst. (TOCS) 32(2), 5 (2014)","journal-title":"ACM Trans. Comput. Syst. (TOCS)"},{"key":"15_CR8","unstructured":"Enck, W., Octeau, D., McDaniel, P., Chaudhuri, S.: A study of android application security. In: USENIX security symposium, vol. 2, p. 2 (2011)"},{"issue":"1","key":"15_CR9","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1109\/MSP.2009.26","volume":"7","author":"W Enck","year":"2009","unstructured":"Enck, W., Ongtang, M., McDaniel, P.: Understanding android security. IEEE Secur. Priv. 7(1), 50\u201357 (2009)","journal-title":"IEEE Secur. Priv."},{"key":"15_CR10","doi-asserted-by":"crossref","unstructured":"Felt, A.P., Chin, E., Hanna, S., Song, D., Wagner, D.: Android permissions demystified. In: Proceedings of the 18th ACM Conference on Computer and Communications Security, pp. 627\u2013638. ACM (2011)","DOI":"10.1145\/2046707.2046779"},{"key":"15_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"296","DOI":"10.1007\/978-3-319-06410-9_21","volume-title":"FM 2014: Formal Methods","author":"H Gunadi","year":"2014","unstructured":"Gunadi, H., Tiu, A.: Efficient runtime monitoring with metric temporal logic: a case study in the android operating system. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 296\u2013311. Springer, Cham (2014). doi:10.1007\/978-3-319-06410-9_21"},{"key":"15_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1007\/3-540-46428-X_20","volume-title":"Fundamental Approaches to Software Engineering","author":"M Huisman","year":"2000","unstructured":"Huisman, M., Jacobs, B.: Java program verification via a hoare logic with abrupt termination. In: Maibaum, T. (ed.) FASE 2000. LNCS, vol. 1783, pp. 284\u2013303. Springer, Heidelberg (2000). doi:10.1007\/3-540-46428-X_20"},{"key":"15_CR13","unstructured":"Jeon, J., Micinski, K.K., Foster, J.S.: Symbolic execution for dalvik bytecode. Technical report, Symdroid (2012)"},{"issue":"6","key":"15_CR14","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2382756.2382798","volume":"37","author":"N Mirzaei","year":"2012","unstructured":"Mirzaei, N., Malek, S., P\u0103s\u0103reanu, C.S., Esfahani, N., Mahmood, R.: Testing android apps through symbolic execution. ACM SIGSOFT Softw. Eng. Notes 37(6), 1\u20135 (2012)","journal-title":"ACM SIGSOFT Softw. Eng. Notes"},{"key":"15_CR15","doi-asserted-by":"crossref","unstructured":"Payet, E., Spoto, F.: An operational semantics for android activities. In: Proceedings of the ACM SIGPLAN 2014 Workshop on Partial Evaluation and Program Manipulation, pp. 121\u2013132. ACM (2014)","DOI":"10.1145\/2543728.2543748"},{"key":"15_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/3-540-49099-X_11","volume-title":"Programming Languages and Systems","author":"A Poetzsch-Heffter","year":"1999","unstructured":"Poetzsch-Heffter, A., M\u00fcller, P.: A programming logic for sequential Java. In: Swierstra, S.D. (ed.) ESOP 1999. LNCS, vol. 1576, pp. 162\u2013176. Springer, Heidelberg (1999). doi:10.1007\/3-540-49099-X_11"},{"key":"15_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/10930755_3","volume-title":"Theorem Proving in Higher Order Logics","author":"CL Quigley","year":"2003","unstructured":"Quigley, C.L.: A programming logic for java bytecode programs. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol. 2758, pp. 41\u201354. Springer, Heidelberg (2003). doi:10.1007\/10930755_3"},{"key":"15_CR18","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: 2002 Proceedings of 17th Annual IEEE Symposium on Logic in Computer Science, pp. 55\u201374. IEEE (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"issue":"3","key":"15_CR19","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1016\/j.istr.2012.10.006","volume":"17","author":"D Schreckling","year":"2013","unstructured":"Schreckling, D., K\u00f6stler, J., Schaff, M.: Kynoid: real-time enforcement of fine-grained, user-defined, and data-centric security policies for android. Inf. Secur. Tech. Rep. 17(3), 71\u201380 (2013)","journal-title":"Inf. Secur. Tech. Rep."},{"key":"15_CR20","unstructured":"Yan, L.-K., Yin, H.: Droidscope: seamlessly reconstructing the OS and dalvik semantic views for dynamic android malware analysis. In: USENIX Security Symposium, pp. 569\u2013584 (2012)"}],"container-title":["Lecture Notes in Computer Science","Computational Science and Its Applications \u2013 ICCSA 2017"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-62407-5_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,22]],"date-time":"2025-06-22T21:08:24Z","timestamp":1750626504000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-62407-5_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319624068","9783319624075"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-62407-5_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"15 July 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ICCSA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computational Science and Its Applications","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Trieste","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2017","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 July 2017","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 July 2017","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"iccsa2017","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.iccsa.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}