{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,6]],"date-time":"2026-01-06T13:27:15Z","timestamp":1767706035763,"version":"3.41.0"},"publisher-location":"Cham","reference-count":20,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319395692"},{"type":"electronic","value":"9783319395708"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"vor","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":[[2016]]},"DOI":"10.1007\/978-3-319-39570-8_14","type":"book-chapter","created":{"date-parts":[[2016,5,24]],"date-time":"2016-05-24T05:04:10Z","timestamp":1464066250000},"page":"212-221","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":67,"title":["Ransomware Steals Your Phone. Formal Methods Rescue It"],"prefix":"10.1007","author":[{"given":"Francesco","family":"Mercaldo","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vittoria","family":"Nardone","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Antonella","family":"Santone","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Corrado Aaron","family":"Visaggio","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,5,24]]},"reference":[{"issue":"1","key":"14_CR1","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1093\/comjnl\/44.1.21","volume":"44","author":"G Anastasi","year":"2001","unstructured":"Anastasi, G., Bartoli, A., Francesco, N.D., Santone, A.: Efficient verification of a multicast protocol for mobile computing. Comput. J. 44(1), 21\u201330 (2001)","journal-title":"Comput. J."},{"key":"14_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"382","DOI":"10.1007\/978-3-319-26362-5_18","volume-title":"Research in Attacks, Intrusions, and Defenses","author":"N Andronio","year":"2015","unstructured":"Andronio, N., Zanero, S., Maggi, F.: HelDroid: dissecting and detecting mobile ransomware. In: Bos, H., Monrose, F., Blanc, G. (eds.) RAID 2015. LNCS, vol. 9404, pp. 382\u2013404. Springer, Heidelberg (2015). doi: 10.1007\/978-3-319-26362-5_18"},{"key":"14_CR3","doi-asserted-by":"crossref","unstructured":"Arp, D., Spreitzenbarth, M., Huebner, M., Gascon, H., Rieck, K.: Drebin: efficient and explainable detection of android malware in your pocket. In: Proceedings of 21st Annual Network and Distributed System Security Symposium (NDSS). IEEE (2014)","DOI":"10.14722\/ndss.2014.23247"},{"issue":"12","key":"14_CR4","doi-asserted-by":"publisher","first-page":"1123","DOI":"10.1002\/(SICI)1097-024X(199910)29:12<1123::AID-SPE275>3.0.CO;2-6","volume":"29","author":"R Barbuti","year":"1999","unstructured":"Barbuti, R., Francesco, N.D., Santone, A., Vaglini, G.: LORETO: a tool for reducing state explosion in verification of LOTOS programs. Softw. Pract. Exper. 29(12), 1123\u20131147 (1999)","journal-title":"Softw. Pract. Exper."},{"key":"14_CR5","doi-asserted-by":"crossref","unstructured":"Battista, P., Mercaldo, F., Nardone, V., Santone, A., Visaggio, C.A.: Identification of android malware families with model checking. In: International Conference on Information Systems Security and Privacy. SCITEPRESS (2016)","DOI":"10.5220\/0005809205420547"},{"key":"14_CR6","doi-asserted-by":"crossref","unstructured":"Canfora, G., Di Sorbo, A., Mercaldo, F., Visaggio, C.: Obfuscation techniques against signature-based detection: a case study. In: Proceedings of Workshop on Mobile System Technologies. IEEE (2015)","DOI":"10.1109\/MST.2015.8"},{"key":"14_CR7","doi-asserted-by":"crossref","unstructured":"Ceccarelli, M., Cerulo, L., Ruvo, G.D., Nardone, V., Santone, A.: Infer gene regulatory networks from time series data with probabilistic model checking. In: 3rd IEEE\/ACM FME Workshop on Formal Methods in Software Engineering, FormaliSE 2015, Florence, Italy, 18 May 2015, pp. 26\u201332. IEEE (2015)","DOI":"10.1109\/FormaliSE.2015.12"},{"key":"14_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1007\/3-540-61474-5_87","volume-title":"Computer Aided Verification","author":"R Cleaveland","year":"1996","unstructured":"Cleaveland, R., Sims, S.: The NCSU concurrency workbench. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 394\u2013397. Springer, Heidelberg (1996)"},{"issue":"2","key":"14_CR9","doi-asserted-by":"publisher","first-page":"513","DOI":"10.1007\/s10270-014-0416-2","volume":"15","author":"N De Francesco","year":"2016","unstructured":"De Francesco, N., Lettieri, G., Santone, A., Vaglini, G.: Heuristic search for equivalence checking. Softw. Syst. Model. 15(2), 513\u2013530 (2016)","journal-title":"Softw. Syst. Model."},{"key":"14_CR10","doi-asserted-by":"crossref","unstructured":"Francesca, G., Santone, A., Vaglini, G., Villani, M.L.: Ant colony optimization for deadlock detection in concurrent systems. In: Proceedings of the 35th Annual IEEE International Computer Software and Applications Conference, COMPSAC 2011, Munich, Germany, 18\u201322 July 2011, pp. 108\u2013117. IEEE (2011)","DOI":"10.1109\/COMPSAC.2011.22"},{"issue":"3","key":"14_CR11","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1016\/S0167-6423(97)00017-8","volume":"30","author":"ND Francesco","year":"1998","unstructured":"Francesco, N.D., Santone, A., Vaglini, G.: State space reduction by non-standard semantics for deadlock analysis. Sci. Comput. Program. 30(3), 309\u2013338 (1998)","journal-title":"Sci. Comput. Program."},{"key":"14_CR12","doi-asserted-by":"crossref","unstructured":"Jacob, G., Filiol, E., Debar, H.: Formalization of viruses and malware through process algebras. In: International Conference on Availability, Reliability and Security (ARES 2010). IEEE (2010)","DOI":"10.1109\/ARES.2010.59"},{"key":"14_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/11506881_11","volume-title":"Intrusion and Malware Detection and Vulnerability Assessment","author":"J Kinder","year":"2005","unstructured":"Kinder, J., Katzenbeisser, S., Schallhart, C., Veith, H.: Detecting malicious code by model checking. In: Julisch, K., Kruegel, C. (eds.) DIMVA 2005. LNCS, vol. 3548, pp. 174\u2013187. Springer, Heidelberg (2005)"},{"key":"14_CR14","doi-asserted-by":"crossref","unstructured":"Mercaldo, F., Nardone, V., Santone, A., Visaggio, C.A.: Download malware? No, thanks. How formal methods can block update attacks. In: 2016 IEEE\/ACM 4th FME Workshop on Formal Methods in Software Engineering (FormaliSE). IEEE (2016)","DOI":"10.1145\/2897667.2897673"},{"key":"14_CR15","series-title":"PHI Series in Computer Science","volume-title":"Communication and Concurrency","author":"R Milner","year":"1989","unstructured":"Milner, R.: Communication and Concurrency. PHI Series in Computer Science. Prentice Hall, Upper Saddle River (1989)"},{"key":"14_CR16","doi-asserted-by":"crossref","unstructured":"Song, F., Touili, T.: Pommade: pushdown model-checking for malware detection. In: Proceedings of the 2013 9th Joint Meeting on Foundations of Software Engineering. ACM (2013)","DOI":"10.1145\/2491411.2494599"},{"key":"14_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"216","DOI":"10.1007\/978-3-319-12736-1_12","volume-title":"Programming Languages and Systems","author":"F Song","year":"2014","unstructured":"Song, F., Touili, T.: Model-checking for android malware detection. In: Garrigue, J. (ed.) APLAS 2014. LNCS, vol. 8858, pp. 216\u2013235. Springer, Heidelberg (2014)"},{"key":"14_CR18","doi-asserted-by":"crossref","unstructured":"Spreitzenbarth, M., Echtler, F., Schreck, T., Freling, F.C., Hoffmann, J.: Mobilesandbox: looking deeper into android applications. In: 28th International ACM Symposium on Applied Computing (SAC). ACM (2013)","DOI":"10.1145\/2480362.2480701"},{"key":"14_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-53932-8_41","volume-title":"Concurrency: Theory, Language, and Architecture","author":"C Stirling","year":"1991","unstructured":"Stirling, C.: An introduction to modal and temporal logics for CCS. In: Ito, T. (ed.) UK\/Japan WS 1989. LNCS, vol. 491, pp. 1\u201320. Springer, Heidelberg (1991)"},{"key":"14_CR20","doi-asserted-by":"crossref","unstructured":"Yang, T., Yang, Y., Qian, K., Lo, D.C.T., Qian, Y., Tao, L.: Automated detection and analysis for android ransomware. In: HPCC\/CSS\/ICESS, pp. 1338\u20131343. IEEE (2015)","DOI":"10.1109\/HPCC-CSS-ICESS.2015.39"}],"container-title":["Lecture Notes in Computer Science","Formal Techniques for Distributed Objects, Components, and Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-39570-8_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,3]],"date-time":"2025-06-03T19:05:46Z","timestamp":1748977546000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-39570-8_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319395692","9783319395708"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-39570-8_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"24 May 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}