{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:37:38Z","timestamp":1761597458110},"reference-count":31,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2013,9,30]],"date-time":"2013-09-30T00:00:00Z","timestamp":1380499200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2014,4]]},"DOI":"10.1007\/s10009-013-0290-1","type":"journal-article","created":{"date-parts":[[2013,9,29]],"date-time":"2013-09-29T08:25:28Z","timestamp":1380443128000},"page":"147-173","source":"Crossref","is-referenced-by-count":22,"title":["Pushdown model checking for malware detection"],"prefix":"10.1007","volume":"16","author":[{"given":"Fu","family":"Song","sequence":"first","affiliation":[]},{"given":"Tayssir","family":"Touili","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2013,9,30]]},"reference":[{"key":"290_CR1","unstructured":"Avast. Free avast antivirus. http:\/\/www.avast.com . Version 6.0.1367"},{"key":"290_CR2","unstructured":"Avira. http:\/\/www.avira.com . Version 12.0.0.849"},{"key":"290_CR3","doi-asserted-by":"crossref","unstructured":"Balakrishnan, G., Gruian, R., Reps, T.W., Teitelbaum, T.: CodeSurfer\/x86-a platform for analyzing x86 executables. In: CC, pp. 250\u2013254 (2005)","DOI":"10.1007\/978-3-540-31985-6_19"},{"key":"290_CR4","doi-asserted-by":"crossref","unstructured":"Balakrishnan, G., Reps, T.W., Kidd, N., Lal, A., Lim, J., Melski, D., Gruian, R., Yong, S.H., Chen, C.-H., Teitelbaum, T.: Model checking x86 executables with CodeSurfer\/x86 and WPDS++. In: CAV, pp. 158\u2013163 (2005)","DOI":"10.1007\/11513988_17"},{"key":"290_CR5","unstructured":"Bergeron, J., Debbabi, M., Desharnais, J., Erhioui, M., Lavoie, Y., Tawbi, N.: Static detection of malicious code in executable programs. In: Symposium on Requirements Engineering for Information Security, pp. 1\u20138 (2001)"},{"key":"290_CR6","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1007\/s11416-008-0102-4","volume":"5","author":"G Bonfante","year":"2009","unstructured":"Bonfante, G., Kaczmarek, M., Marion, J.-Y.: Architecture of a morphological malware detector. J. Comput. Virol. 5, 263\u2013270 (2009)","journal-title":"J. Comput. Virol."},{"key":"290_CR7","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: application to model checking. In: CONCUR\u201997. LNCS 1243 (1997)","DOI":"10.1007\/3-540-63141-0_10"},{"key":"290_CR8","doi-asserted-by":"crossref","unstructured":"Brumley, D., Jager, I., Avgerinos, T., Schwartz, E.J.: BAP: A binary analysis platform. In: Computer Aided Verification (2011)","DOI":"10.1007\/978-3-642-22110-1_37"},{"issue":"3","key":"290_CR9","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1145\/136035.136043","volume":"24","author":"RE Bryant","year":"1992","unstructured":"Bryant, R.E.: Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Comput. Surv. 24(3), 293\u2013318 (1992)","journal-title":"ACM Comput. Surv."},{"key":"290_CR10","unstructured":"Christodorescu, M., Jha, S.: Static analysis of executables to detect malicious patterns. In: 12th USENIX Security, Symposium, pp. 169\u2013186 (2003)"},{"key":"290_CR11","doi-asserted-by":"crossref","unstructured":"Christodorescu, M., Jha, S., Kruegel, C.: Mining specifications of malicious behavior. In: ISEC, pp. 5\u201314 (2008)","DOI":"10.1145\/1342211.1342215"},{"key":"290_CR12","doi-asserted-by":"crossref","unstructured":"Christodorescu, M., Jha, S., Seshia, S.A., Song, D.X., Bryant, R.E.: Semantics-aware malware detection. In: IEEE Symposium on Security and Privacy, pp. 32\u201346 (2005)","DOI":"10.1109\/SP.2005.20"},{"key":"290_CR13","unstructured":"Eric, S.: 10 most destructive computer worms and viruses ever. http:\/\/wildammo.com\/2010\/10\/12\/10-most-destructive-computer-worms-and-viruses-ever (2010)"},{"key":"290_CR14","doi-asserted-by":"crossref","unstructured":"Esparza, J., Kucera, A., Schwoon, S.: Model-checking LTL with regular valuations for pushdown systems. In: TACS, pp. 316\u2013339 (2001)","DOI":"10.1007\/3-540-45500-0_16"},{"issue":"2","key":"290_CR15","doi-asserted-by":"crossref","first-page":"355","DOI":"10.1016\/S0890-5401(03)00139-1","volume":"186","author":"J Esparza","year":"2003","unstructured":"Esparza, J., Kucera, A., Schwoon, S.: Model checking LTL with regular valuations for pushdown systems. Inf. Comput. 186(2), 355\u2013376 (2003)","journal-title":"Inf. Comput."},{"key":"290_CR16","doi-asserted-by":"crossref","unstructured":"Esparza, J., Schwoon, S.: A BDD-based model checker for recursive programs. In: CAV\u201901, pp. 324\u2013336 (2001)","DOI":"10.1007\/3-540-44585-4_30"},{"key":"290_CR17","unstructured":"Gostev, A.: Kaspersky security bulletin, malware evolution 2010. http:\/\/www.securelist.com\/en\/analysis\/204792161\/Kaspersky_Security_Bulletin_Malware_Evolution_2010 . Kaspersky Lab ZAO (2011)"},{"key":"290_CR18","unstructured":"Heavens, V. http:\/\/vx.netlux.org"},{"key":"290_CR19","unstructured":"Hex-Rays. IDAPro (2011)"},{"key":"290_CR20","doi-asserted-by":"crossref","unstructured":"Holzer, A., Kinder, J., Veith, H.: Using verification technology to specify and detect malware. In: EUROCAST, pp. 497\u2013504 (2007)","DOI":"10.1007\/978-3-540-75867-9_63"},{"key":"290_CR21","doi-asserted-by":"crossref","unstructured":"Kinder, J., Katzenbeisser, S., Schallhart, C., Veith, H.: Detecting malicious code by model checking. In: DIMVA, pp. 174\u2013187 (2005)","DOI":"10.1007\/11506881_11"},{"issue":"4","key":"290_CR22","doi-asserted-by":"crossref","first-page":"424","DOI":"10.1109\/TDSC.2008.74","volume":"7","author":"J Kinder","year":"2010","unstructured":"Kinder, J., Katzenbeisser, S., Schallhart, C., Veith, H.: Proactive detection of computer worms using model checking. IEEE Trans. Dependable Secure Comput. 7(4), 424\u2013438 (2010)","journal-title":"IEEE Trans. Dependable Secure Comput."},{"key":"290_CR23","doi-asserted-by":"crossref","unstructured":"Kinder, J., Veith, H.: Jakstab: a static analysis platform for binaries. In: CAV, pp. 423\u2013427 (2008)","DOI":"10.1007\/978-3-540-70545-1_40"},{"key":"290_CR24","doi-asserted-by":"crossref","unstructured":"Lakhotia, A., Boccardo, D.R., Singh, A., Manacero, A.: Context-sensitive analysis of obfuscated x86 executables. In: PEPM, pp. 131\u2013140 (2010)","DOI":"10.1145\/1706356.1706381"},{"issue":"11","key":"290_CR25","doi-asserted-by":"crossref","first-page":"955","DOI":"10.1109\/TSE.2005.120","volume":"31","author":"A Lakhotia","year":"2005","unstructured":"Lakhotia, A., Kumar, E.U., Venable, M.: A method for detecting obfuscated calls in malicious binaries. IEEE Trans. Softw. Eng. 31(11), 955\u2013968 (2005)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"290_CR26","unstructured":"Qihoo 360. http:\/\/www.360.cn"},{"key":"290_CR27","unstructured":"Singh, P.K., Lakhotia, A.: Static verification of worm and virus behavior in binary executables using model checking. In: IAW, pp. 298\u2013300 (2003)"},{"key":"290_CR28","doi-asserted-by":"crossref","unstructured":"Song, F., Touili, T.: Efficient CTL model-checking for pushdown systems. In: CONCUR (2011)","DOI":"10.1007\/978-3-642-23217-6_29"},{"key":"290_CR29","doi-asserted-by":"crossref","unstructured":"Song, F., Touili, T.: Pushdown model checking for malware detection. In: TACAS, pp. 110\u2013125 (2012)","DOI":"10.1007\/978-3-642-28756-5_9"},{"key":"290_CR30","doi-asserted-by":"crossref","unstructured":"Suwimonteerabuth, D., Schwoon, S., Esparza, J.: Efficient algorithms for alternating pushdown systems with an application to the computation of certificate chains. In: ATVA, pp. 141\u2013153 (2006)","DOI":"10.1007\/11901914_13"},{"key":"290_CR31","doi-asserted-by":"crossref","unstructured":"Uezato, Y., Minamide, Y.: Pushdown systems with stack manipulation. In: ATVA\u201913 (2013) (to appear)","DOI":"10.1007\/978-3-319-02444-8_29"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-013-0290-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-013-0290-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-013-0290-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,8,5]],"date-time":"2020-08-05T01:17:54Z","timestamp":1596590274000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-013-0290-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,9,30]]},"references-count":31,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2014,4]]}},"alternative-id":["290"],"URL":"https:\/\/doi.org\/10.1007\/s10009-013-0290-1","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,9,30]]}}}