{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,28]],"date-time":"2025-09-28T04:05:18Z","timestamp":1759032318689},"publisher-location":"Cham","reference-count":37,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319675305"},{"type":"electronic","value":"9783319675312"}],"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":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-67531-2_15","type":"book-chapter","created":{"date-parts":[[2017,9,5]],"date-time":"2017-09-05T09:33:37Z","timestamp":1504604017000},"page":"241-258","source":"Crossref","is-referenced-by-count":12,"title":["Verifying Policy Enforcers"],"prefix":"10.1007","author":[{"given":"Oliviero","family":"Riganelli","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Daniela","family":"Micucci","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Leonardo","family":"Mariani","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yli\u00e8s","family":"Falcone","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,9,6]]},"reference":[{"key":"15_CR1","unstructured":"Android: API Guides. https:\/\/developer.android.com\/guide\/index.html . Accessed 6 May 2017"},{"key":"15_CR2","unstructured":"Android: MediaPlayer. https:\/\/developer.android.com\/reference\/android\/media\/MediaPlayer.html . Accessed 6 May 2017"},{"key":"15_CR3","unstructured":"Android: Package Index. https:\/\/developer.android.com\/reference\/packages.html . Accessed 6 May 2017"},{"key":"15_CR4","unstructured":"Android: The Activity Lifecycle. https:\/\/developer.android.com\/guide\/components\/activities\/activity-lifecycle.html . Accessed 6 May 2017"},{"key":"15_CR5","doi-asserted-by":"crossref","unstructured":"Azim, M.T., Neamtiu, I., Marvel, L.M.: Towards self-healing smartphone software via automated patching. In: Proceedings of the International Conference on Automated Software Engineering (ASE) (2014)","DOI":"10.1145\/2642937.2642955"},{"key":"15_CR6","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P., Larsen, K.G.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"15_CR7","doi-asserted-by":"crossref","unstructured":"Banerjee, A., Chong, L.K., Chattopadhyay, S., Roychoudhury, A.: Detecting energy bugs and hotspots in mobile apps. In: Proceedings of the ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE) (2014)","DOI":"10.1145\/2635868.2635871"},{"key":"15_CR8","doi-asserted-by":"crossref","unstructured":"Bauer, A., K\u00fcster, J., Vegliach, G.: Runtime verification meets Android security. In: Proceedings of the International Symposium on Formal Methods (NFM) (2012)","DOI":"10.1007\/978-3-642-28891-3_18"},{"key":"15_CR9","doi-asserted-by":"crossref","unstructured":"Bauer, L., Ligatti, J., Walker, D.: Composing security policies with polymer. In: Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) (2005)","DOI":"10.1145\/1065010.1065047"},{"key":"15_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/BFb0020949","volume-title":"Hybrid Systems III","author":"J Bengtsson","year":"1996","unstructured":"Bengtsson, J., Larsen, K., Larsson, F., Pettersson, P., Yi, W.: UPPAAL \u2014 a tool suite for automatic verification of real-time systems. In: Alur, R., Henzinger, T.A., Sontag, E.D. (eds.) HS 1995. LNCS, vol. 1066, pp. 232\u2013243. Springer, Heidelberg (1996). doi: 10.1007\/BFb0020949"},{"issue":"4","key":"15_CR11","doi-asserted-by":"crossref","first-page":"239","DOI":"10.1007\/s10207-011-0137-2","volume":"10","author":"N Bielova","year":"2011","unstructured":"Bielova, N., Massacci, F.: Do you really mean what you actually enforced? edited automata revisited. Int. J. Inform. Secur. (IJIS) 10(4), 239\u2013254 (2011)","journal-title":"Int. J. Inform. Secur. (IJIS)"},{"key":"15_CR12","doi-asserted-by":"crossref","unstructured":"Chircop, L., Colombo, C., Pace, G.J.: Device-centric monitoring for mobile device management. In: Proceedings of the International Workshop on Formal Engineering approaches to Software Components and Architectures (FESCA) (2016)","DOI":"10.4204\/EPTCS.205.3"},{"issue":"2","key":"15_CR13","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"EM Clarke","year":"1986","unstructured":"Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst. (TOPLAS) 8(2), 244\u2013263 (1986)","journal-title":"ACM Trans. Program. Lang. Syst. (TOPLAS)"},{"key":"15_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/978-3-642-10665-1_5","volume-title":"Cloud Computing","author":"Y Dai","year":"2009","unstructured":"Dai, Y., Xiang, Y., Zhang, G.: Self-healing and hybrid diagnosis in cloud computing. In: Jaatun, M.G., Zhao, G., Rong, C. (eds.) CloudCom 2009. LNCS, vol. 5931, pp. 45\u201356. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-10665-1_5"},{"key":"15_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/978-3-319-23820-3_24","volume-title":"Runtime Verification","author":"P Daian","year":"2015","unstructured":"Daian, P., Falcone, Y., Meredith, P., \u015eerb\u0103nu\u0163\u0103, T.F., Shiriashi, S., Iwai, A., Rosu, G.: RV-Android: efficient parametric android runtime verification, a brief tutorial. In: Bartocci, E., Majumdar, R. (eds.) RV 2015. LNCS, vol. 9333, pp. 342\u2013357. Springer, Cham (2015). doi: 10.1007\/978-3-319-23820-3_24"},{"key":"15_CR16","doi-asserted-by":"crossref","unstructured":"Falcone, Y., Currea, S., Jaber, M.: Runtime verification and enforcement for Android applications with RV-Droid. In: Proceedings of the International Conference on Runtime Verification (RV) (2012)","DOI":"10.1007\/978-3-642-35632-2_11"},{"issue":"3","key":"15_CR17","doi-asserted-by":"crossref","first-page":"349","DOI":"10.1007\/s10009-011-0196-8","volume":"14","author":"Y Falcone","year":"2012","unstructured":"Falcone, Y., Fernandez, J.C., Mounier, L.: What can you verify and enforce at runtime? Int. J. Softw. Tools Technol. Transfer 14(3), 349\u2013382 (2012)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"15_CR18","first-page":"2","volume":"123","author":"Y Falcone","year":"2016","unstructured":"Falcone, Y., J\u00e9ron, T., Marchand, H., Pinisetty, S.: Runtime enforcement of regular timed properties by suppressing and delaying events. Syst. Control Lett. 123, 2\u201341 (2016)","journal-title":"Syst. Control Lett."},{"issue":"3","key":"15_CR19","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1007\/s10703-011-0114-4","volume":"38","author":"Y Falcone","year":"2011","unstructured":"Falcone, Y., Mounier, L., Fernandez, J.C., Richier, J.L.: Runtime enforcement monitors: composition, synthesis, and enforcement abilities. Formal Methods Syst. Des. 38(3), 223\u2013262 (2011)","journal-title":"Formal Methods Syst. Des."},{"key":"15_CR20","doi-asserted-by":"crossref","unstructured":"Guo, C., Zhang, J., Yan, J., Zhang, Z., Zhang, Y.: Characterizing and detecting resource leaks in android applications. In: Proceedings of the International Conference on Automated Software Engineering (ASE) (2013)","DOI":"10.1109\/ASE.2013.6693097"},{"key":"15_CR21","doi-asserted-by":"crossref","first-page":"413","DOI":"10.1007\/978-1-4757-3472-0_16","volume-title":"The Origin of Concurrent Programming","author":"CAR Hoare","year":"1978","unstructured":"Hoare, C.A.R.: Communicating sequential processes. In: Hansen, P.B. (ed.) The Origin of Concurrent Programming, pp. 413\u2013443. Springer, New York (1978)"},{"key":"15_CR22","doi-asserted-by":"crossref","unstructured":"Hyrynsalmi, S., Suominen, A., M\u00e4kil\u00e4, T., Knuutila, T.: Mobile application ecosystems: an analysis of android ecosystem. In: Encyclopedia of E-Commerce Development, Implementation, and Management, chap. 100, vol. II, pp. 1418\u20131434. IGI Global (2016)","DOI":"10.4018\/978-1-4666-9787-4.ch100"},{"issue":"1","key":"15_CR23","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1016\/j.cosrev.2012.01.001","volume":"6","author":"R Khoury","year":"2012","unstructured":"Khoury, R., Tawbi, N.: Which security policies are enforceable by runtime monitors? a survey. Comput. Sci. Rev. 6(1), 27\u201345 (2012)","journal-title":"Comput. Sci. Rev."},{"key":"15_CR24","doi-asserted-by":"crossref","unstructured":"K\u00fcster, J., Bauer, A.: Monitoring real android malware. In: Proceedings of the International Conference on Runtime Verification (RV) (2015)","DOI":"10.1007\/978-3-319-23820-3_9"},{"key":"15_CR25","doi-asserted-by":"crossref","unstructured":"Li, L., Bissyand\u00e9, T.F., Octeau, D., Klein, J.: DroidRA: taming reflection to support whole-program analysis of android apps. In: Proceedings of the International Symposium on Software Testing and Analysis (ISSTA) (2016)","DOI":"10.1145\/2931037.2931044"},{"issue":"1","key":"15_CR26","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1007\/s10207-004-0046-8","volume":"4","author":"J Ligatti","year":"2005","unstructured":"Ligatti, J., Bauer, L., Walker, D.: Edit automata: enforcement mechanisms for run-time security policies. Int. J. Inform. Secur. 4(1), 2\u201316 (2005)","journal-title":"Int. J. Inform. Secur."},{"key":"15_CR27","doi-asserted-by":"crossref","unstructured":"Ligatti, J., Bauer, L., Walker, D.: Run-time enforcement of nonsafety policies. ACM Trans. Inform. Syst. Secur. (TISSEC) 12(3), 19:1\u201319:41 (2009)","DOI":"10.1145\/1455526.1455532"},{"issue":"3","key":"15_CR28","first-page":"219","volume":"2","author":"NA Lynch","year":"1988","unstructured":"Lynch, N.A., Tuttle, M.R.: An introduction to input\/output automata. CWI Q. 2(3), 219\u2013246 (1988)","journal-title":"CWI Q."},{"key":"15_CR29","doi-asserted-by":"crossref","unstructured":"Magalh\u00e3es, J.P., Silva, L.M.: SH\u00d5WA: a self-healing framework for web-based applications. ACM Trans. Auton. Adapt. Syst. 10(1), 4:1\u20134:28 (2015)","DOI":"10.1145\/2700325"},{"issue":"3","key":"15_CR30","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1007\/s10703-014-0215-y","volume":"45","author":"S Pinisetty","year":"2014","unstructured":"Pinisetty, S., Falcone, Y., J\u00e9ron, T., Marchand, H., Rollet, A., Nguena-Timo, O.: Runtime enforcement of timed properties revisited. Formal Methods Syst. Des. 45(3), 381\u2013422 (2014). https:\/\/doi.org\/10.1007\/s10703-014-0215-y","journal-title":"Formal Methods Syst. Des."},{"key":"15_CR31","doi-asserted-by":"crossref","unstructured":"Riganelli, O., Micucci, D., Mariani, L.: Healing data loss problems in android apps. In: Proceedings of the International Workshop on Software Faults (IWSF), Co-located with the International Symposium on Software Reliability Engineering (ISSRE) (2016)","DOI":"10.1109\/ISSREW.2016.50"},{"key":"15_CR32","doi-asserted-by":"crossref","unstructured":"Riganelli, O., Micucci, D., Mariani, L.: Policy enforcement with proactive libraries. In: Proceedings of the International Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS) (2017)","DOI":"10.1109\/SEAMS.2017.9"},{"issue":"1","key":"15_CR33","doi-asserted-by":"crossref","first-page":"30","DOI":"10.1145\/353323.353382","volume":"3","author":"FB Schneider","year":"2000","unstructured":"Schneider, F.B.: Enforceable security policies. ACM Trans. Inform. Syst. Secur. (TISSEC) 3(1), 30\u201350 (2000)","journal-title":"ACM Trans. Inform. Syst. Secur. (TISSEC)"},{"key":"15_CR34","doi-asserted-by":"crossref","unstructured":"Shan, Z., Azim, T., Neamtiu, I.: Finding resume and restart errors in android applications. In: Proceedings of the ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA) (2016)","DOI":"10.1145\/2983990.2984011"},{"key":"15_CR35","doi-asserted-by":"crossref","unstructured":"Sidiroglou, S., Laadan, O., Perez, C., Viennot, N., Nieh, J., Keromytis, A.D.: ASSURE: automatic software self-healing using rescue points. In: Proceedings of the International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS) (2009)","DOI":"10.1145\/1508244.1508250"},{"key":"15_CR36","doi-asserted-by":"crossref","unstructured":"Wei, L., Liu, Y., Cheung, S.C.: Taming android fragmentation: characterizing and detecting compatibility issues for android apps. In: Proceedings of the IEEE\/ACM International Conference on Automated Software Engineering (ASE) (2016)","DOI":"10.1145\/2970276.2970312"},{"issue":"11","key":"15_CR37","doi-asserted-by":"crossref","first-page":"1054","DOI":"10.1109\/TSE.2016.2547385","volume":"42","author":"T Wu","year":"2016","unstructured":"Wu, T., Liu, J., Xu, Z., Guo, C., Zhang, Y., Yan, J., Zhang, J.: Light-weight, inter-procedural and callback-aware resource leak detection for android apps. IEEE Trans. Softw. Eng. (TSE) 42(11), 1054\u20131076 (2016)","journal-title":"IEEE Trans. Softw. Eng. (TSE)"}],"container-title":["Lecture Notes in Computer Science","Runtime Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-67531-2_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,3]],"date-time":"2019-10-03T04:19:31Z","timestamp":1570076371000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-67531-2_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319675305","9783319675312"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-67531-2_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}