{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,12]],"date-time":"2026-02-12T15:10:45Z","timestamp":1770909045048,"version":"3.50.1"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032104434","type":"print"},{"value":"9783032104441","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,11,12]],"date-time":"2025-11-12T00:00:00Z","timestamp":1762905600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,11,12]],"date-time":"2025-11-12T00:00:00Z","timestamp":1762905600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-10444-1_3","type":"book-chapter","created":{"date-parts":[[2025,11,11]],"date-time":"2025-11-11T06:58:49Z","timestamp":1762844329000},"page":"34-51","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Reachability Analysis of\u00a0Upper-Stack Manipulating Binary Code"],"prefix":"10.1007","author":[{"given":"Shijie","family":"Lin","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tayssir","family":"Touili","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,11,12]]},"reference":[{"issue":"2","key":"3_CR1","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1007\/s10703-014-0207-y","volume":"45","author":"PA Abdulla","year":"2014","unstructured":"Abdulla, P.A., Atig, M.F., Rezine, O., Stenman, J.: Budget-bounded model-checking pushdown systems. Form. Methods Syst. Des. 45(2), 273\u2013301 (2014)","journal-title":"Form. Methods Syst. Des."},{"key":"3_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/978-3-642-37036-6_28","volume-title":"Programming Languages and Systems","author":"J Alglave","year":"2013","unstructured":"Alglave, J., Kroening, D., Nimal, V., Tautschnig, M.: Software verification for weak memory via program transformation. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 512\u2013532. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-37036-6_28"},{"key":"3_CR3","doi-asserted-by":"crossref","unstructured":"Anderson, P.: Codesurfer\/path inspector. In: 20th IEEE International Conference on Software Maintenance, 2004. Proceedings, p. 508 (2004)","DOI":"10.1109\/ICSM.2004.1357853"},{"key":"3_CR4","unstructured":"Atig, M.F.: Global model checking of ordered multi-pushdown systems. In: Lodaya, K., Mahajan, M., Eds., IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010) (Dagstuhl, Germany, 2010), vol.\u00a08 of Leibniz International Proceedings in Informatics (LIPIcs), Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, pp.\u00a0216\u2013227 (2010)"},{"key":"3_CR5","unstructured":"Atig, M.F., Bouajjani, A., Kumar, K., Saivasan, P.: On bounded reachability analysis of shared memory systems. In: Leibniz International Proceedings in Informatics, LIPIcs 29, pp. 611\u2013623 (2014)"},{"key":"3_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1007\/978-3-540-31985-6_19","volume-title":"Compiler Construction","author":"G Balakrishnan","year":"2005","unstructured":"Balakrishnan, G., Gruian, R., Reps, T., Teitelbaum, T.: CodeSurfer\/x86\u2014a platform for analyzing x86 executables. In: Bodik, R. (ed.) CC 2005. LNCS, vol. 3443, pp. 250\u2013254. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-31985-6_19"},{"key":"3_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/978-3-540-24723-4_2","volume-title":"Compiler Construction","author":"G Balakrishnan","year":"2004","unstructured":"Balakrishnan, G., Reps, T.: Analyzing memory accesses in x86 executables. In: Duesterwald, E. (ed.) CC 2004. LNCS, vol. 2985, pp. 5\u201323. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24723-4_2"},{"key":"3_CR8","doi-asserted-by":"publisher","first-page":"6","DOI":"10.1145\/1749608.1749612","volume":"32","author":"G Balakrishnan","year":"2010","unstructured":"Balakrishnan, G., Reps, T.: WYSINWYX: what you see is not what you execute. ACM Trans. Program. Lang. Syst. 32, 6 (2010)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"3_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1007\/11513988_17","volume-title":"Computer Aided Verification","author":"G Balakrishnan","year":"2005","unstructured":"Balakrishnan, G., Reps, T., Kidd, N., Lal, A., Lim, J., Melski, D., Gruian, R., Yong, S., Chen, C.-H., Teitelbaum, T.: Model checking x86 executables with CodeSurfer\/x86 and WPDS++. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 158\u2013163. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11513988_17"},{"key":"3_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/3-540-63141-0_10","volume-title":"CONCUR \u201997: Concurrency Theory","author":"A Bouajjani","year":"1997","unstructured":"Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: application to model-checking. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol. 1243, pp. 135\u2013150. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/3-540-63141-0_10"},{"key":"3_CR11","doi-asserted-by":"crossref","unstructured":"Carayol, A., Hague, M.: Saturation algorithms for model-checking pushdown systems. arXiv preprintarXiv:1405.5593 (2014)","DOI":"10.4204\/EPTCS.151.1"},{"key":"3_CR12","doi-asserted-by":"crossref","unstructured":"Carotenuto, D., Murano, A., Peron, A.: 2-visibly pushdown automata. In: International Conference on Developments in Language Theory, pp.\u00a0132\u2013144. Springer (2007)","DOI":"10.1007\/978-3-540-73208-2_15"},{"issue":"5","key":"3_CR13","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"E Clarke","year":"2003","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50(5), 752\u2013794 (2003)","journal-title":"J. ACM"},{"key":"3_CR14","doi-asserted-by":"crossref","unstructured":"Esparza, J., Hansel, D., Rossmanith, P., Schwoon, S.: Efficient algorithms for model checking pushdown systems. In: International Conference on Computer Aided Verification (2000)","DOI":"10.1007\/10722167_20"},{"key":"3_CR15","doi-asserted-by":"crossref","unstructured":"La Torre, S., Madhusudan, P., Parlato, G.: A robust class of context-sensitive languages. In: Proceedings - 22nd Annual IEEE Symposiumon Logic in Computer Science, LICS 2007 (2007), Proceedings - Symposium on Logic in Computer Science, pp.\u00a0161\u2013170. 22nd Annual IEEE Symposium on Logic in Computer Science, LICS 2007 ; Conference date: 10-07-2007 Through 14-07-2007","DOI":"10.1109\/LICS.2007.9"},{"key":"3_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"477","DOI":"10.1007\/978-3-642-02658-4_36","volume-title":"Computer Aided Verification","author":"S La Torre","year":"2009","unstructured":"La Torre, S., Madhusudan, P., Parlato, G.: Reducing context-bounded concurrent reachability to sequential reachability. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 477\u2013492. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_36"},{"key":"3_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/978-3-642-23217-6_14","volume-title":"CONCUR 2011 \u2013 Concurrency Theory","author":"S La Torre","year":"2011","unstructured":"La Torre, S., Napoli, M.: Reachability of multistack pushdown systems with scope-bounded matching relations. In: Katoen, J.-P., K\u00f6nig, B. (eds.) CONCUR 2011. LNCS, vol. 6901, pp. 203\u2013218. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-23217-6_14"},{"key":"3_CR18","unstructured":"Lang, M.: Resource-bounded reachability on pushdown systems. Master\u2019s thesis, RWTH Aachen University (2011)"},{"key":"3_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/978-3-319-53733-7_33","volume-title":"Language and Automata Theory and Applications","author":"A Pommellet","year":"2017","unstructured":"Pommellet, A., Diaz, M., Touili, T.: Reachability analysis of pushdown systems with an upper stack. In: Drewes, F., Mart\u00edn-Vide, C., Truthe, B. (eds.) LATA 2017. LNCS, vol. 10168, pp. 447\u2013459. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-53733-7_33"},{"key":"3_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-540-77050-3_4","volume-title":"FSTTCS 2007: Foundations of Software Technology and Theoretical Computer Science","author":"T Reps","year":"2007","unstructured":"Reps, T., Lal, A., Kidd, N.: Program analysis using weighted pushdown systems. In: Arvind, V., Prasad, S. (eds.) FSTTCS 2007. LNCS, vol. 4855, pp. 23\u201351. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-77050-3_4"},{"key":"3_CR21","doi-asserted-by":"crossref","unstructured":"Seth, A.: Global reachability in bounded phase multi-stack pushdown systems. In: International Conference on Computer Aided Verification (2010)","DOI":"10.1007\/978-3-642-14295-6_53"},{"key":"3_CR22","doi-asserted-by":"crossref","unstructured":"Shu, L., Shi, J., Ye, X., Jiang, N., Li, Y.: A new parallel approach for reachability analysis of pushdown models. In: Proceedings of the 2017 International Conference on Management Engineering, Software Engineering and Service Sciences, pp.\u00a0113\u2013118 (2017)","DOI":"10.1145\/3034950.3034984"},{"key":"3_CR23","unstructured":"Song, F.: On pushdown systems model checking: application to malware detection and software model-checking. PhD thesis, 2013. Th\u00e8se de doctorat dirig\u00e9e par Touili, Tayssir Informatique Paris 7 (2013)"},{"key":"3_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"418","DOI":"10.1007\/978-3-642-32759-9_34","volume-title":"FM 2012: Formal Methods","author":"F Song","year":"2012","unstructured":"Song, F., Touili, T.: Efficient malware detection using model-checking. In: Giannakopoulou, D., M\u00e9ry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 418\u2013433. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-32759-9_34"},{"key":"3_CR25","doi-asserted-by":"crossref","unstructured":"Song, F., Touili, T.: Pushdown model checking for malware detection. In: Flanagan, C., K\u00f6nig, B., Eds., Tools and Algorithms for the Construction and Analysis of Systems, pp.\u00a0110\u2013125. Springer, Berlin, Heidelberg (2012)","DOI":"10.1007\/978-3-642-28756-5_9"},{"key":"3_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"416","DOI":"10.1007\/978-3-642-36742-7_29","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"F Song","year":"2013","unstructured":"Song, F., Touili, T.: LTL model-checking for malware detection. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 416\u2013431. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-36742-7_29"},{"key":"3_CR27","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, ESEC\/FSE 2013, Association for Computing Machinery, pp.\u00a0607\u2013610. New York, NY, USA (2013)","DOI":"10.1145\/2491411.2494599"},{"key":"3_CR28","doi-asserted-by":"crossref","unstructured":"Touili, T., Ye, X.: LTL model checking of self modifying code (2019)","DOI":"10.1109\/ICECCS.2019.00008"},{"key":"3_CR29","doi-asserted-by":"crossref","unstructured":"Touili, T., Ye, X.: SMODIC: a model checker for self-modifying code. In: Proceedings of the 17th International Conference on Availability, Reliability and Security, ARES \u201922, Association for Computing Machinery. New York, NY, USA (2022)","DOI":"10.1145\/3538969.3538978"},{"issue":"05","key":"3_CR30","doi-asserted-by":"publisher","first-page":"507","DOI":"10.1142\/S0129054122500290","volume":"34","author":"T Touili","year":"2023","unstructured":"Touili, T., Ye, X.: Reachability analysis of self modifying code. Int. J. Found. Comput. Sci. 34(05), 507\u2013536 (2023)","journal-title":"Int. J. Found. Comput. Sci."}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-10444-1_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,12]],"date-time":"2026-02-12T14:07:02Z","timestamp":1770905222000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-10444-1_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,12]]},"ISBN":["9783032104434","9783032104441"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-10444-1_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,11,12]]},"assertion":[{"value":"12 November 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SEFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Software Engineering and Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Toledo","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Spain","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 November 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14 November 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sefm2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/sefm-conference.github.io\/2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}