{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,22]],"date-time":"2025-11-22T11:10:44Z","timestamp":1763809844145,"version":"3.37.3"},"reference-count":55,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"12","license":[{"start":{"date-parts":[[2019,12,1]],"date-time":"2019-12-01T00:00:00Z","timestamp":1575158400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2019,12,1]],"date-time":"2019-12-01T00:00:00Z","timestamp":1575158400000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2019,12,1]],"date-time":"2019-12-01T00:00:00Z","timestamp":1575158400000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"funder":[{"name":"H2020 EU","award":["#675320","#700294"],"award-info":[{"award-number":["#675320","#700294"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IIEEE Trans. Software Eng."],"published-print":{"date-parts":[[2019,12,1]]},"DOI":"10.1109\/tse.2018.2834344","type":"journal-article","created":{"date-parts":[[2018,5,8]],"date-time":"2018-05-08T18:59:34Z","timestamp":1525805974000},"page":"1230-1252","source":"Crossref","is-referenced-by-count":46,"title":["LEILA: Formal Tool for Identifying Mobile Malicious Behaviour"],"prefix":"10.1109","volume":"45","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0049-1279","authenticated-orcid":false,"given":"Gerardo","family":"Canfora","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fabio","family":"Martinelli","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9425-1657","authenticated-orcid":false,"given":"Francesco","family":"Mercaldo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vittoria","family":"Nardone","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2634-4456","authenticated-orcid":false,"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":"263","reference":[{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-12736-1_12"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1145\/2491411.2494599"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1145\/2484313.2484355"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-005-1634-6"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1145\/2886012"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1007\/s11390-017-1786-z"},{"key":"ref37","first-page":"418","article-title":"Efficient malware detection using model-checking","author":"song","year":"2001","journal-title":"Proc Int Symp Formal Methods"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1007\/11506881_11"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1016\/j.ins.2006.03.008"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1145\/2931037.2931044"},{"key":"ref28","first-page":"212","article-title":"Ransomware steals your phone. Formal methods rescue it","author":"mercaldo","year":"2016","journal-title":"Proc Int Conf Formal Techn Distrib Objects Compon Syst"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1109\/ARES.2016.35"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1109\/FormaliSE.2017.4"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1109\/MST.2015.8"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1109\/DICTAP.2016.7544005"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-39570-8_14"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2014.23247"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1145\/2897667.2897673"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-26362-5_18"},{"key":"ref23","doi-asserted-by":"crossref","first-page":"1808","DOI":"10.1145\/2480362.2480701","article-title":"Mobilesandbox: Looking deeper into android applications","author":"spreitzenbarth","year":"2013","journal-title":"Proc 28th ACM Symp Applied Computing"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1109\/BWCCA.2010.85"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2012.16"},{"key":"ref50","first-page":"543","article-title":"Effective inter-component communication mapping in android: An essential step towards holistic security analysis","author":"octeau","year":"2013","journal-title":"Proc 22nd USENIX Secur Symp"},{"key":"ref51","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2015.48"},{"key":"ref55","doi-asserted-by":"publisher","DOI":"10.1145\/2897845.2897856"},{"key":"ref54","first-page":"1","article-title":"On the need of precise inter-app ICC classification for detecting android malware collusions","author":"elish","year":"2015","journal-title":"Proc IEEE Mobile Secur Technol Conjunction IEEE Symp Secur Privacy"},{"key":"ref53","doi-asserted-by":"publisher","DOI":"10.1109\/TrustCom.2014.50"},{"key":"ref52","doi-asserted-by":"publisher","DOI":"10.1145\/2619091"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1145\/2666356.2594299"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1145\/2660267.2660357"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1109\/ARES.2010.59"},{"journal-title":"Data Leakage in Mobile Malware The What the Why and the How","year":"2017","author":"georgios kambourakis","key":"ref12"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1109\/TIFS.2013.2290431"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69850-0_12"},{"journal-title":"Communication and Concurrency","year":"1989","author":"milner","key":"ref15"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1006\/jcss.1999.1660"},{"key":"ref17","first-page":"2","article-title":"An introduction to modal and temporal logics for ccs","author":"stirling","year":"1989","journal-title":"Proceedings of the UK\/Japan workshop on Concurrency theory language and architecture"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-25150-9_33"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1016\/B978-044450813-3\/50026-6"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1109\/TIFS.2013.2290431"},{"key":"ref3","article-title":"Review on security threats for mobile devices and significant countermeasures on securing android mobiles","author":"nishani","year":"2015","journal-title":"Automated Enterprise Systems for Maximizing Business Performance"},{"key":"ref6","first-page":"82","article-title":"ADAM: An automatic and extensible platform to stress test android anti-virus systems","author":"zheng","year":"2012","journal-title":"Detection of Intrusions and Malware and Vulnerability Assessment"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1145\/2484313.2484355"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-04283-1_6"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1145\/2046614.2046619"},{"key":"ref49","doi-asserted-by":"publisher","DOI":"10.1109\/IJCNN.2017.7966078"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-60876-1_12"},{"key":"ref46","doi-asserted-by":"publisher","DOI":"10.1109\/SPW.2016.25"},{"key":"ref45","doi-asserted-by":"publisher","DOI":"10.1109\/TIFS.2016.2523912"},{"key":"ref48","doi-asserted-by":"publisher","DOI":"10.1145\/3029806.3029825"},{"key":"ref47","doi-asserted-by":"publisher","DOI":"10.1145\/2897845.2897860"},{"key":"ref42","doi-asserted-by":"publisher","DOI":"10.5220\/0005809205420547"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2017.2697848"},{"key":"ref44","doi-asserted-by":"publisher","DOI":"10.1109\/TDSC.2016.2536605"},{"key":"ref43","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/j.cose.2016.04.009","article-title":"An HMM and structural entropy based detector for android malware","volume":"61","author":"canfora","year":"2016","journal-title":"Comput Secur"}],"container-title":["IEEE Transactions on Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/32\/8930349\/08356128.pdf?arnumber=8356128","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,22]],"date-time":"2022-08-22T20:40:48Z","timestamp":1661200848000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/8356128\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,12,1]]},"references-count":55,"journal-issue":{"issue":"12"},"URL":"https:\/\/doi.org\/10.1109\/tse.2018.2834344","relation":{},"ISSN":["0098-5589","1939-3520","2326-3881"],"issn-type":[{"type":"print","value":"0098-5589"},{"type":"electronic","value":"1939-3520"},{"type":"electronic","value":"2326-3881"}],"subject":[],"published":{"date-parts":[[2019,12,1]]}}}