{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:09:46Z","timestamp":1776305386672,"version":"3.50.1"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319941103","type":"print"},{"value":"9783319941110","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","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":[[2018]]},"DOI":"10.1007\/978-3-319-94111-0_7","type":"book-chapter","created":{"date-parts":[[2018,6,15]],"date-time":"2018-06-15T15:07:44Z","timestamp":1529075264000},"page":"115-132","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":26,"title":["Joint Forces for Memory Safety Checking"],"prefix":"10.1007","author":[{"given":"Marek","family":"Chalupa","sequence":"first","affiliation":[]},{"given":"Jan","family":"Strej\u010dek","sequence":"additional","affiliation":[]},{"given":"Martina","family":"Vitovsk\u00e1","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,6,16]]},"reference":[{"key":"7_CR1","unstructured":"Andersen, L.O.: Program Analysis and Specialization for the C Programming Language. Ph.D thesis, DIKU, University of Copenhagen (1994)"},{"key":"7_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/978-3-540-31984-9_2","volume-title":"Fundamental Approaches to Software Engineering","author":"D Beyer","year":"2005","unstructured":"Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: Checking memory safety with blast. In: Cerioli, M. (ed.) FASE 2005. LNCS, vol. 3442, pp. 2\u201318. Springer, Heidelberg (2005). \nhttps:\/\/doi.org\/10.1007\/978-3-540-31984-9_2"},{"key":"7_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/978-3-642-22110-1_16","volume-title":"Computer Aided Verification","author":"D Beyer","year":"2011","unstructured":"Beyer, D., Keremoglu, M.E.: CPAchecker: a tool for configurable software verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 184\u2013190. Springer, Heidelberg (2011). \nhttps:\/\/doi.org\/10.1007\/978-3-642-22110-1_16"},{"key":"7_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/978-3-319-23404-5_12","volume-title":"Model Checking Software","author":"D Beyer","year":"2015","unstructured":"Beyer, D., L\u00f6we, S., Wendler, P.: Benchmarking and resource measurement. In: Fischer, B., Geldenhuys, J. (eds.) SPIN 2015. LNCS, vol. 9232, pp. 160\u2013178. Springer, Cham (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-319-23404-5_12"},{"key":"7_CR5","unstructured":"Cadar, C., Dunbar, D., Engler, D.R.: KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In: 8th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2008, 8\u201310 December 2008, San Diego, California, USA, Proceedings, pp. 209\u2013224. USENIX Association (2008)"},{"key":"7_CR6","doi-asserted-by":"crossref","unstructured":"Carter, M., He, S., Whitaker, J., Rakamari\u0107, Z., Emmi, M.: SMACK software verification toolchain. In: Proceedings of the 38th IEEE\/ACM International Conference on Software Engineering (ICSE) Companion, pp. 589\u2013592. ACM (2016)","DOI":"10.1145\/2889160.2889163"},{"key":"7_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"442","DOI":"10.1007\/978-3-319-89963-3_29","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Chalupa","year":"2018","unstructured":"Chalupa, M., Vitovsk\u00e1, M., Strej\u010dek, J.: SYMBIOTIC\u00a05: boosted instrumentation. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10806, pp. 442\u2013446. Springer, Cham (2018). \nhttps:\/\/doi.org\/10.1007\/978-3-319-89963-3_29"},{"key":"7_CR8","doi-asserted-by":"crossref","unstructured":"Cytron, R., Ferrante, J., Rosen, B.K., Wegman, M.N., Zadeck, F.K.: An efficient method of computing static single assignment form. In: Conference Record of the Sixteenth Annual ACM Symposium on Principles of Programming Languages, Austin, Texas, USA, 11\u201313 January 1989, pp. 25\u201335. ACM (1989)","DOI":"10.1145\/75277.75280"},{"key":"7_CR9","doi-asserted-by":"crossref","unstructured":"Dhurjati, D., Adve, V.: Backwards-compatible array bounds checking for C with very low overhead. In: Proceedings of the 28th International Conference on Software Engineering, ICSE 2006, pp. 162\u2013171. ACM (2006)","DOI":"10.1145\/1134285.1134309"},{"key":"7_CR10","doi-asserted-by":"crossref","unstructured":"Dhurjati, D., Kowshik, S., Adve, V.: SAFECode: enforcing alias analysis for weakly typed languages. In: PLDI 2006: Proceedings of the 2006 ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 144\u2013157. ACM (2006)","DOI":"10.1145\/1133981.1133999"},{"key":"7_CR11","doi-asserted-by":"crossref","unstructured":"Dor, N., Rodeh, M., Sagiv, M.: Detecting memory errors via static pointer analysis (preliminary experience). In: Proceedings of the 1998 ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering, PASTE 1998, pp. 27\u201334. ACM (1998)","DOI":"10.1145\/277631.277637"},{"key":"7_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/3-540-12925-1_33","volume-title":"International Symposium on Programming","author":"J Ferrante","year":"1984","unstructured":"Ferrante, J., Ottenstein, K.J., Warren, J.D.: The program dependence graph and its use in optimization. In: Paul, M., Robinet, B. (eds.) Programming 1984. LNCS, vol. 167, pp. 125\u2013132. Springer, Heidelberg (1984). \nhttps:\/\/doi.org\/10.1007\/3-540-12925-1_33"},{"key":"7_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1007\/978-3-319-21690-4_20","volume-title":"Computer Aided Verification","author":"A Gurfinkel","year":"2015","unstructured":"Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The SeaHorn verification framework. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 343\u2013361. Springer, Cham (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-319-21690-4_20"},{"issue":"1","key":"7_CR14","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1016\/j.scico.2005.02.005","volume":"58","author":"SZ Guyer","year":"2005","unstructured":"Guyer, S.Z., Lin, C.: Error checking with client-driven pointer analysis. Sci. Comput. Program. 58(1), 83\u2013114 (2005)","journal-title":"Sci. Comput. Program."},{"key":"7_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/978-3-642-39799-8_2","volume-title":"Computer Aided Verification","author":"M Heizmann","year":"2013","unstructured":"Heizmann, M., Hoenicke, J., Podelski, A.: Software model checking for people who love automata. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 36\u201352. Springer, Heidelberg (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-642-39799-8_2"},{"key":"7_CR16","doi-asserted-by":"crossref","unstructured":"Hind, M.: Pointer analysis: haven\u2019t we solved this problem yet? In: Proceedings of the 2001 ACM SIGPLAN-SIGSOFT Workshop on Program Analysis For Software Tools and Engineering, PASTE 2001, Snowbird, Utah, USA, 18\u201319 June 2001, pp. 54\u201361. ACM (2001)","DOI":"10.1145\/379605.379665"},{"key":"7_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/978-3-319-49052-6_13","volume-title":"Hardware and Software: Verification and Testing","author":"L Hol\u00edk","year":"2016","unstructured":"Hol\u00edk, L., Kotoun, M., Peringer, P., \u0160okov\u00e1, V., Trt\u00edk, M., Vojnar, T.: Predator shape analysis tool suite. In: Bloem, R., Arbel, E. (eds.) HVC 2016. LNCS, vol. 10028, pp. 202\u2013209. Springer, Cham (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-319-49052-6_13"},{"issue":"1","key":"7_CR18","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1145\/77606.77608","volume":"12","author":"S Horwitz","year":"1990","unstructured":"Horwitz, S., Reps, T.W., Binkley, D.W.: Interprocedural slicing using dependence graphs. ACM Trans. Program. Lang. Syst. 12(1), 26\u201360 (1990)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"7_CR19","unstructured":"Jones, R.W.M., Kelly, P.H.J.: Backwards-compatible bounds checking for arrays and pointers in C programs. In: AADEBUG, pp. 13\u201326 (1997)"},{"issue":"7","key":"7_CR20","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1145\/360248.360252","volume":"19","author":"JC King","year":"1976","unstructured":"King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385\u2013394 (1976)","journal-title":"Commun. ACM"},{"key":"7_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/978-3-642-54862-8_26","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Kroening","year":"2014","unstructured":"Kroening, D., Tautschnig, M.: CBMC \u2013 C bounded model checker. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 389\u2013391. Springer, Heidelberg (2014). \nhttps:\/\/doi.org\/10.1007\/978-3-642-54862-8_26"},{"key":"7_CR22","doi-asserted-by":"crossref","unstructured":"Lattner, C., Adve, V.: LLVM: a compilation framework for lifelong program analysis & transformation. In: 2nd IEEE \/ ACM International Symposium on Code Generation and Optimization (CGO 2004), 20\u201324 March 2004, San Jose, CA, USA, CGO 2004, pp. 75\u201388. IEEE Computer Society (2004)","DOI":"10.1109\/CGO.2004.1281665"},{"issue":"6","key":"7_CR23","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1145\/1064978.1065027","volume":"40","author":"C Lattner","year":"2005","unstructured":"Lattner, C., Adve, V.: Automatic pool allocation: Improving performance by controlling data structure layout in the heap. SIGPLAN Not. 40(6), 129\u2013142 (2005)","journal-title":"SIGPLAN Not."},{"key":"7_CR24","unstructured":"The LLVM compiler infrastructure (2017). \nhttp:\/\/llvm.org"},{"key":"7_CR25","unstructured":"Map2check tool (2018). \nhttps:\/\/map2check.github.io\/"},{"key":"7_CR26","doi-asserted-by":"crossref","unstructured":"Midi, D., Payer, M., Bertino, E.: Memory safety for embedded devices with nesCheck. In: Proceedings of the 2017 ACM on Asia Conference on Computer and Communications Security, ASIA CCS 2017, pp. 127\u2013139. ACM (2017)","DOI":"10.1145\/3052973.3053014"},{"issue":"1","key":"7_CR27","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1145\/565816.503286","volume":"37","author":"GC Necula","year":"2002","unstructured":"Necula, G.C., McPeak, S., Weimer, W.: CCured: type-safe retrofitting of legacy code. SIGPLAN Not. 37(1), 128\u2013139 (2002)","journal-title":"SIGPLAN Not."},{"key":"7_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"458","DOI":"10.1007\/978-3-662-46681-0_44","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Nutz","year":"2015","unstructured":"Nutz, A., Dietsch, D., Mohamed, M.M., Podelski, A.: ULTIMATE KOJAK with memory safety checks. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 458\u2013460. Springer, Heidelberg (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-662-46681-0_44"},{"key":"7_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/3-540-45306-7_10","volume-title":"Compiler Construction","author":"N Rinetzky","year":"2001","unstructured":"Rinetzky, N., Sagiv, M.: Interprocedural shape analysis for recursive programs. In: Wilhelm, R. (ed.) CC 2001. LNCS, vol. 2027, pp. 133\u2013149. Springer, Heidelberg (2001). \nhttps:\/\/doi.org\/10.1007\/3-540-45306-7_10"},{"key":"7_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"934","DOI":"10.1007\/978-3-662-49674-9_64","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"HO Rocha","year":"2016","unstructured":"Rocha, H.O., Barreto, R.S., Cordeiro, L.C.: Hunting memory bugs in C programs with Map2Check. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 934\u2013937. Springer, Heidelberg (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-662-49674-9_64"},{"key":"7_CR31","unstructured":"Ruwase, O., Lam, M.S.: A practical dynamic buffer overflow detector. In: Proceedings of the Network and Distributed System Security Symposium, NDSS 2004, San Diego, California, USA, pp. 159\u2013169. The Internet Society (2004)"},{"key":"7_CR32","doi-asserted-by":"crossref","unstructured":"Saeed, A., Ahmadinia, A., Just, M.: Tag-protector: an effective and dynamic detection of out-of-bound memory accesses. In: Proceedings of the Third Workshop on Cryptography and Security in Computing Systems, CS2 2016, pp. 31\u201336. ACM (2016)","DOI":"10.1145\/2858930.2858936"},{"key":"7_CR33","unstructured":"Serebryany, K., Bruening, D., Potapenko, A., Vyukov, D.: Addresssanitizer: a fast address sanity checker. In: Proceedings of the 2012 USENIX Conference on Annual Technical Conference, USENIX ATC 2012, pp. 28\u201328. USENIX Association (2012)"},{"key":"7_CR34","unstructured":"Vitovsk\u00e1, M.: Instrumentation of LLVM IR. Master\u2019s thesis, Masaryk University, Faculty of Informatics, Brno (2018)"},{"key":"7_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"320","DOI":"10.1007\/11599555_32","volume-title":"Embedded Software and Systems","author":"Y Xia","year":"2005","unstructured":"Xia, Y., Luo, J., Zhang, M.: Detecting memory access errors with flow-sensitive conditional range analysis. In: Yang, L.T., Zhou, X., Zhao, W., Wu, Z., Zhu, Y., Lin, M. (eds.) ICESS 2005. LNCS, vol. 3820, pp. 320\u2013331. Springer, Heidelberg (2005). \nhttps:\/\/doi.org\/10.1007\/11599555_32"},{"key":"7_CR36","doi-asserted-by":"crossref","unstructured":"Yong, S.H., Horwitz, S.: Protecting C programs from attacks via invalid pointer dereferences. In: Proceedings of the 9th European Software Engineering Conference Held Jointly with 11th ACM SIGSOFT International Symposium on Foundations of Software Engineering, ESEC\/FSE-11, pp. 307\u2013316. ACM (2003)","DOI":"10.1145\/940071.940113"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-94111-0_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2018,6,15]],"date-time":"2018-06-15T15:13:13Z","timestamp":1529075593000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-94111-0_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319941103","9783319941110"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-94111-0_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]}}}