{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,12]],"date-time":"2025-11-12T14:02:05Z","timestamp":1762956125807,"version":"3.37.3"},"reference-count":47,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2019,8,6]],"date-time":"2019-08-06T00:00:00Z","timestamp":1565049600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2019,8,6]],"date-time":"2019-08-06T00:00:00Z","timestamp":1565049600000},"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":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2020,4]]},"DOI":"10.1007\/s10009-019-00526-2","type":"journal-article","created":{"date-parts":[[2019,8,6]],"date-time":"2019-08-06T14:44:33Z","timestamp":1565102673000},"page":"115-133","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Joint forces for memory safety checking revisited"],"prefix":"10.1007","volume":"22","author":[{"given":"Marek","family":"Chalupa","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5873-403X","authenticated-orcid":false,"given":"Jan","family":"Strej\u010dek","sequence":"additional","affiliation":[]},{"given":"Martina","family":"Vitovsk\u00e1","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,8,6]]},"reference":[{"key":"526_CR1","unstructured":"Andersen, L.O.: Program Analysis and Specialization for the C Programming Language. PhD thesis, DIKU, University of Copenhagen (1994)"},{"key":"526_CR2","doi-asserted-by":"crossref","unstructured":"Beyer, D., Erkan Keremoglu, M.: CPAchecker: a tool for configurable software verification. In: Computer Aided Verification\u201423rd International Conference, CAV 2011, Snowbird, UT, USA, July 14\u201320, 2011. Proceedings, volume 6806 of Lecture Notes in Computer Science, pp. 184\u2013190. Springer (2011)","DOI":"10.1007\/978-3-642-22110-1_16"},{"key":"526_CR3","doi-asserted-by":"crossref","unstructured":"Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: Checking memory safety with blast. In: Fundamental Approaches to Software Engineering, 8th International Conference, FASE 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, April 4\u20138, 2005, Proceedings, volume 3442 of Lecture Notes in Computer Science, pp. 2\u201318. Springer (2005)","DOI":"10.1007\/978-3-540-31984-9_2"},{"key":"526_CR4","doi-asserted-by":"crossref","unstructured":"Beyer, D., L\u00f6we, S., Wendler, P.: Benchmarking and resource measurement. In: Model Checking Software\u201422nd International Symposium, SPIN 2015, Stellenbosch, South Africa, August 24\u201326, 2015, Proceedings, volume 9232 of Lecture Notes in Computer Science, pp. 160\u2013178. Springer (2015)","DOI":"10.1007\/978-3-319-23404-5_12"},{"key":"526_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, December 8\u201310, 2008, San Diego, California, USA, Proceedings, pp. 209\u2013224. USENIX Association (2008)"},{"key":"526_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":"526_CR7","doi-asserted-by":"crossref","unstructured":"Chalupa, M., Strej\u010dek, J., Vitovsk\u00e1, M.: Joint forces for memory safety checking. In: Gallardo, M.d.M., Merino, P., (Eds.), Model Checking Software\u2014-25th International Symposium, SPIN 2018, Malaga, Spain, June 20\u201322, 2018, Proceedings, volume 10869 of Lecture Notes in Computer Science, pp. 115\u2013132. Springer (2018)","DOI":"10.1007\/978-3-319-94111-0_7"},{"key":"526_CR8","doi-asserted-by":"crossref","unstructured":"Chalupa, M., Vitovsk\u00e1, M., Strej\u010dek, J.: Symbiotic 5: boosted instrumentation (competition contribution). In: Tools and Algorithms for the Construction and Analysis of Systems\u201424th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14\u201320, 2018, Proceedings, Part II, volume 10806 of Lecture Notes in Computer Science, pp. 442\u2013446. Springer (2018)","DOI":"10.1007\/978-3-319-89963-3_29"},{"key":"526_CR9","doi-asserted-by":"crossref","unstructured":"Chebaro, O., Kosmatov, N., Giorgetti, A., Julliand, J.: The SANTE tool: value analysis, program slicing and test generation for C program debugging. In: Tests and Proofs\u20145th International Conference, TAP 2011, Zurich, Switzerland, June 30\u2013July 1, 2011. Proceedings, volume 6706 of Lecture Notes in Computer Science, pp. 78\u201383. Springer (2011)","DOI":"10.1007\/978-3-642-21768-5_7"},{"issue":"1","key":"526_CR10","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/s10515-013-0127-x","volume":"21","author":"O Chebaro","year":"2014","unstructured":"Chebaro, O., Cuoq, P., Kosmatov, N., Marre, B., Pacalet, A., Williams, N., Yakobowski, B.: Behind the scenes in sante: a combination of static and dynamic analyses. Autom. Softw. Eng. 21(1), 107\u2013143 (2014)","journal-title":"Autom. Softw. Eng."},{"key":"526_CR11","unstructured":"Clang: a C language family frontend for LLVM (2018). \nhttp:\/\/clang.llvm.org\n\n. Accessed 5 Nov 2018"},{"key":"526_CR12","unstructured":"Cytron, R., Ferrante, J., Rosen, B.K., Wegman, M.N., Kenneth Zadeck, F.: 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, January 11\u201313, 1989, pp. 25\u201335. ACM (1989)"},{"key":"526_CR13","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 \u201906, pp. 162\u2013171. ACM (2006)","DOI":"10.1145\/1134285.1134309"},{"key":"526_CR14","doi-asserted-by":"crossref","unstructured":"Dhurjati, D., Kowshik, S., Adve, V.: SAFECode: enforcing alias analysis for weakly typed languages. In PLDI \u201906: Proceedings of the 2006 ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 144\u2013157. ACM (2006)","DOI":"10.1145\/1133981.1133999"},{"key":"526_CR15","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 \u201998, pp. 27\u201334. ACM (1998)","DOI":"10.1145\/277631.277637"},{"key":"526_CR16","doi-asserted-by":"crossref","unstructured":"Dudka, K., Peringer, P., Vojnar, T.: Byte-precise verification of low-level list manipulation. In: Logozzo, F, F\u00e4hndrich, M. (Eds.), Static Analysis\u201420th International Symposium, SAS 2013, Seattle, WA, USA, June 20\u201322, 2013. Proceedings, volume 7935 of Lecture Notes in Computer Science, pp. 215\u2013237. Springer (2013)","DOI":"10.1007\/978-3-642-38856-9_13"},{"key":"526_CR17","doi-asserted-by":"crossref","unstructured":"Ferrante, J., Ottenstein, K.J., Warren, J.D.: The program dependence graph and its use in optimization. In: International Symposium on Programming, 6th Colloquium, Toulouse, April 17\u201319, 1984, Proceedings, volume 167 of Lecture Notes in Computer Science, pp. 125\u2013132. Springer (1984)","DOI":"10.1007\/3-540-12925-1_33"},{"key":"526_CR18","doi-asserted-by":"crossref","unstructured":"Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The SeaHorn verification framework. In: Computer Aided Verification\u201427th International Conference, CAV 2015, San Francisco, CA, USA, July 18\u201324, 2015, Proceedings, Part I, volume 9206 of Lecture Notes in Computer Science, pp. 343\u2013361. Springer (2015)","DOI":"10.1007\/978-3-319-21690-4_20"},{"issue":"1","key":"526_CR19","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":"526_CR20","doi-asserted-by":"crossref","unstructured":"Heizmann, M., Hoenicke, J., Podelski, A.: Software model checking for people who love automata. In: Computer Aided Verification\u201425th International Conference, CAV 2013, Saint Petersburg, Russia, July 13\u201319, 2013. Proceedings, volume 8044 of Lecture Notes in Computer Science, pp. 36\u201352. Springer (2013)","DOI":"10.1007\/978-3-642-39799-8_2"},{"key":"526_CR21","doi-asserted-by":"crossref","unstructured":"Hind, M.: Pointer analysis: Haven\u2019t we solved this problem yet? In: Proceedings of the 2001 ACM SIGPLAN\u2013SIGSOFT Workshop on Program Analysis For Software Tools and Engineering, PASTE\u201901, Snowbird, Utah, USA, June 18\u201319, 2001, pp. 54\u201361. ACM (2001)","DOI":"10.1145\/379605.379665"},{"key":"526_CR22","doi-asserted-by":"publisher","first-page":"848","DOI":"10.1145\/325478.325519","volume":"21","author":"M Hind","year":"1999","unstructured":"Hind, M., Burke, M., Carini, P., Choi, J.-D.: Interprocedural pointer alias analysis. ACM Trans. Program. Lang. Syst. (TOPLAS) 21, 848\u2013894 (1999)","journal-title":"ACM Trans. Program. Lang. Syst. (TOPLAS)"},{"key":"526_CR23","doi-asserted-by":"crossref","unstructured":"Hol\u00edk, L., Kotoun, M., Peringer, P., \u0160okov\u00e1, V., Trt\u00edk, M., Vojnar, T.: Predator shape analysis tool suite. In: Proceedings of HVC 2016, volume 10028 of Lecture Notes in Computer Science, pp. 202\u2013209. Springer (2016)","DOI":"10.1007\/978-3-319-49052-6_13"},{"issue":"1","key":"526_CR24","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":"526_CR25","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":"526_CR26","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":"526_CR27","unstructured":"Kroening, D., Tautschnig, Mi.: CBMC\u2013C bounded model checker\u2014(competition contribution). In: Tools and Algorithms for the Construction and Analysis of Systems\u201420th International Conference, TACAS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5\u201313, 2014. Proceedings, volume 8413 of Lecture Notes in Computer Science, pp. 389\u2013391. Springer (2014)"},{"key":"526_CR28","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 \u201904, pp. 75\u201388. IEEE Computer Society (2004)"},{"issue":"6","key":"526_CR29","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":"526_CR30","unstructured":"Map2check tool (2018). \nhttps:\/\/map2check.github.io\/\n\n. Accessed 26 Feb 2017"},{"key":"526_CR31","doi-asserted-by":"crossref","unstructured":"Menezes, R., Rocha, H., Cordeiro, L.C., Barreto, R.S.: Map2check using LLVM and KLEE\u2014(competition contribution). In: Beyer, D., Huisman, M., (Eds.), Tools and Algorithms for the Construction and Analysis of Systems\u201424th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14\u201320, 2018, Proceedings, Part II, volume 10806 of Lecture Notes in Computer Science, pp. 437\u2013441. Springer (2018)","DOI":"10.1007\/978-3-319-89963-3_28"},{"key":"526_CR32","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 \u201917, pp. 127\u2013139. ACM (2017)","DOI":"10.1145\/3052973.3053014"},{"key":"526_CR33","doi-asserted-by":"crossref","unstructured":"Nagarakatte, S., Zhao, J., Martin, M.M.K., Zdancewic, S.: Softbound: highly compatible and complete spatial memory safety for c. In: Proceedings of the 30th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI \u201909, pp. 245\u2013258. ACM (2009)","DOI":"10.1145\/1543135.1542504"},{"issue":"8","key":"526_CR34","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1145\/1837855.1806657","volume":"45","author":"S Nagarakatte","year":"2010","unstructured":"Nagarakatte, S., Zhao, J., Martin, M.M.K., Zdancewic, S.: Cets: Compiler enforced temporal safety for c. SIGPLAN Not. 45(8), 31\u201340 (2010)","journal-title":"SIGPLAN Not."},{"issue":"1","key":"526_CR35","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":"526_CR36","doi-asserted-by":"crossref","unstructured":"Nutz, A., Dietsch, D., Mohamed, M.M., Podelski, A.: ULTIMATE KOJAK with memory safety checks\u2014(competition contribution). In: Tools and Algorithms for the Construction and Analysis of Systems\u201421st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11\u201318, 2015. Proceedings, volume 9035 of Lecture Notes in Computer Science, pp. 458\u2013460 (2015)","DOI":"10.1007\/978-3-662-46681-0_44"},{"key":"526_CR37","doi-asserted-by":"crossref","unstructured":"Rinetzky, N., Sagiv, S.: Interprocedural shape analysis for recursive programs. In: Compiler Construction, 10th International Conference, CC 2001 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001 Genova, Italy, April 2\u20136, 2001, Proceedings, volume 2027 of Lecture Notes in Computer Science, pp. 133\u2013149. Springer (2001)","DOI":"10.1007\/3-540-45306-7_10"},{"key":"526_CR38","doi-asserted-by":"crossref","unstructured":"Rocha, H.O., Barreto, R.S., Cordeiro, L.C.: Hunting memory bugs in C programs with map2check\u2014(competition contribution). In: Tools and Algorithms for the Construction and Analysis of Systems\u201422nd International Conference, TACAS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2\u20138, 2016, Proceedings, volume 9636 of Lecture Notes in Computer Science, pp. 934\u2013937. Springer (2016)","DOI":"10.1007\/978-3-662-49674-9_64"},{"key":"526_CR39","unstructured":"Rodrigues, R.E., Campos, V.H.S., Pereira, F.M.Q.: A fast and low-overhead technique to secure programs against integer overflows. In: Proceedings of the 2013 IEEE\/ACM International Symposium on Code Generation and Optimization, CGO 2013, Shenzhen, China, February 23\u201327, 2013, pp. 33:1\u201333:11. IEEE Computer Society (2013)"},{"key":"526_CR40","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, CA, USA, pp. 159\u2013169. The Internet Society (2004)"},{"key":"526_CR41","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 \u201916, pp. 31\u201336. ACM (2016)","DOI":"10.1145\/2858930.2858936"},{"key":"526_CR42","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\u201912, pp. 28\u201328. USENIX Association (2012)"},{"key":"526_CR43","unstructured":"$$\\text{Softbound} + \\text{ cets }$$: Complete and compatible full memory safety for c (2018). \nhttps:\/\/www.cs.rutgers.edu\/~santosh.nagarakatte\/softbound\/\n\n. Accessed 5 Nov 2018"},{"key":"526_CR44","unstructured":"The LLVM compiler infrastructure (2017). \nhttp:\/\/llvm.org\n\n. Accessed 17 Feb 2017"},{"key":"526_CR45","unstructured":"Vitovsk\u00e1, M., Chalupa, M., Strej\u010dek, J.: SBT-instrumentation: a tool for configurable instrumentation of LLVM bitcode (2018). \narXiv:1810.12617"},{"key":"526_CR46","doi-asserted-by":"crossref","unstructured":"Xia, Y., Luo, J., Zhang, M.: Detecting memory access errors with flow-sensitive conditional range analysis. In: Embedded Software and Systems: Second International Conference, ICESS 2005, Xi\u2019an, China, December 16\u201318, 2005. Proceedings, volume 3820 of Lecture Notes in Computer Science, pp. 320\u2013331. Springer (2005)","DOI":"10.1007\/11599555_32"},{"key":"526_CR47","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":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-019-00526-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-019-00526-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-019-00526-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,8,4]],"date-time":"2020-08-04T23:19:12Z","timestamp":1596583152000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-019-00526-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,8,6]]},"references-count":47,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2020,4]]}},"alternative-id":["526"],"URL":"https:\/\/doi.org\/10.1007\/s10009-019-00526-2","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"type":"print","value":"1433-2779"},{"type":"electronic","value":"1433-2787"}],"subject":[],"published":{"date-parts":[[2019,8,6]]},"assertion":[{"value":"6 August 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}