{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,6]],"date-time":"2025-04-06T15:10:09Z","timestamp":1743952209953,"version":"3.40.3"},"reference-count":58,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2012,8,4]],"date-time":"2012-08-04T00:00:00Z","timestamp":1344038400000},"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,2]]},"DOI":"10.1007\/s10009-012-0256-8","type":"journal-article","created":{"date-parts":[[2012,8,3]],"date-time":"2012-08-03T15:25:38Z","timestamp":1344007538000},"page":"81-102","source":"Crossref","is-referenced-by-count":0,"title":["Symbolic object code analysis"],"prefix":"10.1007","volume":"16","author":[{"given":"Jan Tobias","family":"M\u00fchlberg","sequence":"first","affiliation":[]},{"given":"Gerald","family":"L\u00fcttgen","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2012,8,4]]},"reference":[{"key":"256_CR1","doi-asserted-by":"crossref","unstructured":"Balakrishnan, G., Reps, T.: Recency-abstraction for heap-allocated storage. In: SAS \u201906. LNCS, vol. 4134, pp. 221\u2013239. Springer, Berlin (2006)","DOI":"10.1007\/11823230_15"},{"key":"256_CR2","doi-asserted-by":"crossref","unstructured":"Balakrishnan, G., Reps, T., Melski, D., Teitelbaum, T.: WYSINWYX: what you see is not what you execute. In: VSTTE \u201908. LNCS, vol. 4171, pp. 202\u2013213. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-69149-5_22"},{"issue":"4","key":"256_CR3","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1145\/1218063.1217943","volume":"40","author":"T Ball","year":"2006","unstructured":"Ball, T., Bounimova, E., Cook, B., Levin, V., Lichtenberg, J., McGarvey, C., Ondrusek, B., Rajamani, S.K., Ustuner, A.: Thorough static analysis of device drivers. SIGOPS Oper. Syst. Rev. 40(4), 73\u201385 (2006)","journal-title":"SIGOPS Oper. Syst. Rev."},{"key":"256_CR4","doi-asserted-by":"crossref","unstructured":"Ball, T., Rajamani, S.K.: Automatically validating temporal safety properties of interfaces. In: SPIN \u201901. LNCS, vol. 2057, pp. 103\u2013122. Springer, Berlin (2001)","DOI":"10.1007\/3-540-45139-0_7"},{"key":"256_CR5","unstructured":"Barry, R.: FreeRTOS: A portable, open source, mini real time kernel (2010) http:\/\/www.freertos.org\/"},{"issue":"1","key":"256_CR6","doi-asserted-by":"crossref","first-page":"166","DOI":"10.1145\/227595.227603","volume":"43","author":"RS Boyer","year":"1996","unstructured":"Boyer, R.S., Yu, Y.: Automated proofs of object code for a widely used microprocessor. J. ACM 43(1), 166\u2013192 (1996)","journal-title":"J. ACM"},{"key":"256_CR7","doi-asserted-by":"crossref","unstructured":"Brummayer, R., Biere, A., Lonsing, F.: BTOR: bit-precise modelling of word-level problems for model checking. In: SMT \u201908\/BPR \u201908, pp. 33\u201338. ACM, New York (2008)","DOI":"10.1145\/1512464.1512472"},{"issue":"1","key":"256_CR8","doi-asserted-by":"crossref","first-page":"289","DOI":"10.1145\/1594834.1480917","volume":"44","author":"C Calcagno","year":"2009","unstructured":"Calcagno, C., Distefano, D., O\u2019Hearn, P., Yang, H.: Compositional shape analysis by means of bi-abduction. SIGPLAN Not. 44(1), 289\u2013300 (2009)","journal-title":"SIGPLAN Not."},{"key":"256_CR9","doi-asserted-by":"crossref","unstructured":"Chou, A., Yang, J., Chelf, B., Hallem, S., Engler, D.R.: An empirical study of operating system errors. In: SOSP \u201901, pp. 73\u201388. ACM, New York (2001)","DOI":"10.1145\/502034.502042"},{"key":"256_CR10","doi-asserted-by":"crossref","unstructured":"Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: TACAS \u201904. LNCS, vol. 2988, pp. 168\u2013176. Springer, Berlin (2004)","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"256_CR11","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Kroening, D., Sharygina, N., Yorav, K.: SATABS: SAT-based predicate abstraction for ANSI-C. In: TACAS \u201905. LNCS, vol. 3440, pp. 570\u2013574. Springer, Berlin (2005)","DOI":"10.1007\/978-3-540-31980-1_40"},{"key":"256_CR12","doi-asserted-by":"crossref","unstructured":"Cohen, E., Dahlweid, M., Hillebrand, M., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: VCC: a practical system for verifying concurrent C. In: TPHOLs \u201909. LNCS, vol. 5674, pp. 23\u201342. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-03359-9_2"},{"issue":"7","key":"256_CR13","doi-asserted-by":"crossref","first-page":"1165","DOI":"10.1109\/TCAD.2008.923410","volume":"27","author":"V D\u2019Silva","year":"2008","unstructured":"D\u2019Silva, V., Kroening, D., Weissenbacher, G.A.: A survey of automated techniques for formal software verification. IEEE Trans. Comput. Aided Design Integr. Circuits Syst. 27(7), 1165\u20131178 (2008)","journal-title":"IEEE Trans. Comput. Aided Design Integr. Circuits Syst."},{"key":"256_CR14","unstructured":"Dutertre, B., de Moura, L.: The Yices SMT solver. Technical Report 01\/2006, SRI (2006). http:\/\/yices.csl.sri.com\/tool-paper.pdf"},{"key":"256_CR15","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. In: POPL \u201905, pp. 110\u2013121. ACM, New York (2005)","DOI":"10.1145\/1047659.1040315"},{"key":"256_CR16","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Klarlund, N., Sen, K.: DART: directed automated random testing. In: PLDI \u201905, pp. 213\u2013223. ACM, New York (2005)","DOI":"10.1145\/1065010.1065036"},{"key":"256_CR17","unstructured":"Godefroid, P., Levin, M.Y., Molnar, D.: Automated whitebox fuzz testing. In: NDSS \u201908. Internet Society (ISOC) (2008)"},{"key":"256_CR18","doi-asserted-by":"crossref","unstructured":"Hansen, T., Schachte, P., S\u00f8ndergaard, H.: State joining and splitting for the symbolic execution of binaries. In: RV \u201909. LNCS, vol. 5779, pp. 76\u201392. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-04694-0_6"},{"key":"256_CR19","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Necula, G.C., Sutre, G., Weimer, W.: Temporal-safety proofs for systems code. In: CAV \u201902. LNCS, vol. 2402, pp. 526\u2013538. Springer, Berlin (2002)","DOI":"10.1007\/3-540-45657-0_45"},{"issue":"3","key":"256_CR20","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1093\/comjnl\/23.3.223","volume":"23","author":"RN Horspool","year":"1980","unstructured":"Horspool, R.N., Marovac, N.: An approach to the problem of detranslation of computer programs. Comput. J. 23(3), 223\u2013229 (1980)","journal-title":"Comput. J."},{"issue":"1","key":"256_CR21","doi-asserted-by":"crossref","first-page":"26","DOI":"10.1145\/77606.77608","volume":"12","author":"S Horwitz","year":"1990","unstructured":"Horwitz, S., Reps, T., Binkley, D.: Interprocedural slicing using dependence graphs. ACM TOPLAS 12(1), 26\u201360 (1990)","journal-title":"ACM TOPLAS"},{"key":"256_CR22","unstructured":"International Organization for Standardization: The C99 standard, ISO\/IEC 9899:1999. Technical Report 9899:1999, International Organization for Standardization (1999)"},{"key":"256_CR23","doi-asserted-by":"crossref","unstructured":"Jacobs, B., Smans, J., Piessens, F.: A quick tour of the VeriFast program verifier. In: APLAS \u201910. LNCS, vol. 6461, pp. 304\u2013311. Springer, Berlin (2010)","DOI":"10.1007\/978-3-642-17164-2_21"},{"issue":"6","key":"256_CR24","doi-asserted-by":"crossref","first-page":"38","DOI":"10.1145\/1064978.1065016","volume":"40","author":"R Jhala","year":"2005","unstructured":"Jhala, R., Majumdar, R.: Path slicing. SIGPLAN Not. 40(6), 38\u201347 (2005)","journal-title":"SIGPLAN Not."},{"key":"256_CR25","doi-asserted-by":"crossref","unstructured":"Josh Berdine, C.C., O\u2019Hearn, P.W.: Symbolic execution with separation logic. In: APLAS \u201905. LNCS, vol. 3780, pp. 52\u201368. Springer, Berlin (2005)","DOI":"10.1007\/11575467_5"},{"key":"256_CR26","doi-asserted-by":"crossref","unstructured":"Kim, M., Kim, Y.: Concolic testing of the multi-sector read operation for flash memory file system. In: SBMF \u201909. LNCS, vol. 5902, pp. 251\u2013265. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-10452-7_17"},{"key":"256_CR27","unstructured":"Kinder, J., Veith, H.: Precise static analysis of untrusted driver binaries. In: FMCAD \u201910, pp. 43\u201350. IEEE (2010)"},{"issue":"7","key":"256_CR28","doi-asserted-by":"crossref","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"},{"issue":"3","key":"256_CR29","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1016\/0164-1212(90)90094-3","volume":"13","author":"B Korel","year":"1990","unstructured":"Korel, B., Laski, J.: Dynamic slicing of computer programs. J. Syst. Softw. 13(3), 187\u2013195 (1990)","journal-title":"J. Syst. Softw."},{"key":"256_CR30","unstructured":"Koshy, J.: LibElf: http:\/\/wiki.freebsd.org\/LibElf (2009)"},{"key":"256_CR31","doi-asserted-by":"crossref","unstructured":"Kroening, D., Sharygina, N., Tonetta, S., Tsitovich, A., Wintersteiger, C.M.: Loop summarization using abstract transformers. In: ATVA \u201908. LNCS, vol. 5311, pp. 111\u2013125. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-88387-6_10"},{"key":"256_CR32","unstructured":"Kroening, D., Strichman, O.: Decision Procedures, Springer, Berlin (2008)"},{"key":"256_CR33","unstructured":"Ku, K.: Software model-checking: benchmarking and techniques for buffer overflow analysis. Master\u2019s thesis, U. Toronto (2008)"},{"key":"256_CR34","doi-asserted-by":"crossref","unstructured":"Leung, A., George, L.: Static single assignment form for machine code. In: PLDI \u201999, pp. 204\u2013214. ACM, New York (1999)","DOI":"10.1145\/301631.301667"},{"key":"256_CR35","doi-asserted-by":"crossref","unstructured":"Leven, P., Mehler, T., Edelkamp, S.: Directed error detection in C++ with the assembly-level model checker StEAM. In: Model Checking Software. LNCS, vol. 2989, pp. 39\u201356. Springer, Berlin (2004)","DOI":"10.1007\/978-3-540-24732-6_4"},{"key":"256_CR36","unstructured":"M\u00fchlberg, J.T.: Model Checking Pointer Safety in Compiled Programs. PhD thesis, U. York http:\/\/etheses.whiterose.ac.uk\/841\/ (2009)"},{"key":"256_CR37","unstructured":"M\u00fchlberg, J.T., Freitas, L.: Verifying FreeRTOS: from requirements to binary code. In: AVoCS \u201911, vol. CS-TR-1272 of Computing Science Technical Reports, Newcastle University. Short paper (2011)"},{"key":"256_CR38","doi-asserted-by":"crossref","unstructured":"M\u00fchlberg, J.T., L\u00fcttgen, G.: BLASTing Linux code. In: FMICS \u201906. LNCS, vol. 4346, pp. 211\u2013226. Springer, Berlin (2006)","DOI":"10.1007\/978-3-540-70952-7_14"},{"key":"256_CR39","doi-asserted-by":"crossref","unstructured":"M\u00fchlberg, J.T., L\u00fcttgen, G.: Verifying compiled file system code. In: SBMF \u201909. LNCS, vol. 5902, pp. 306\u2013320. Springer, Berlin (2009). A full version has been accepted for publication in Springer\u2019s Formal Aspects of Computing journal","DOI":"10.1007\/978-3-642-10452-7_21"},{"issue":"6","key":"256_CR40","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1145\/1273442.1250746","volume":"42","author":"N Nethercote","year":"2007","unstructured":"Nethercote, N., Seward, J.: Valgrind: a framework for heavyweight dynamic binary instrumentation. SIGPLAN Not. 42(6), 89\u2013100 (2007)","journal-title":"SIGPLAN Not."},{"key":"256_CR41","doi-asserted-by":"crossref","unstructured":"Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer, Berlin (1999)","DOI":"10.1007\/978-3-662-03811-6"},{"key":"256_CR42","doi-asserted-by":"crossref","unstructured":"Noll, T., Schlich, B.: Delayed nondeterminism in model checking embedded systems assembly code. In: Hardware and Software: Verification and Testing. LNCS, vol. 4899, pp. 185\u2013201. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-77966-7_16"},{"key":"256_CR43","doi-asserted-by":"crossref","unstructured":"P\u01ces\u01cereanu, C.S., Mehlitz, P.C., Bushnell, D.H., Gundy-Burlet, K., Lowry, M., Person, S., Pape, M.: Combining unit-level symbolic execution and system-level concrete execution for testing NASA software. In: ISSTA \u201908, pp. 15\u201326. ACM, New York (2008)","DOI":"10.1145\/1390630.1390635"},{"issue":"4","key":"256_CR44","doi-asserted-by":"crossref","first-page":"339","DOI":"10.1007\/s10009-009-0118-1","volume":"11","author":"CS P\u01ces\u01cereanu","year":"2009","unstructured":"P\u01ces\u01cereanu, C.S., Visser, W.: A survey of new trends in symbolic execution for software testing and analysis. STTT 11(4), 339\u2013353 (2009)","journal-title":"STTT"},{"key":"256_CR45","unstructured":"Rational Purify. IBM Corp., http:\/\/www.ibm.com\/software\/awdtools\/purify\/"},{"key":"256_CR46","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In : LICS \u201902, pp. 55\u201374. IEEE (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"key":"256_CR47","doi-asserted-by":"crossref","unstructured":"Rungta, N., Mercer, E.G., Visser, W.: Efficient testing of concurrent programs with abstraction-guided symbolic execution. In: SPIN \u201909. LNCS, vol. 5578, pp. 174\u2013191. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-02652-2_16"},{"key":"256_CR48","doi-asserted-by":"crossref","unstructured":"Schlich, B., Kowalewski, S.: [mc]square: a model checker for microcontroller code. In: ISOLA \u201906, pp. 466\u2013473. IEEE (2006)","DOI":"10.1109\/ISoLA.2006.62"},{"key":"256_CR49","doi-asserted-by":"crossref","unstructured":"Sen, K., Marinov, D., Agha, G.: CUTE: a concolic unit testing engine for C. In: ESEC\/FSE-13, pp. 263\u2013272. ACM, New York (2005)","DOI":"10.21236\/ADA482657"},{"key":"256_CR50","unstructured":"Tool Interface Standards (TIS) Committee: Executable and Linking Format (ELF) specification version 1.2 (1995). http:\/\/refspecs.freestandards.org\/elf\/"},{"key":"256_CR51","unstructured":"Valgrind\u2014debugging and profiling Linux programs. http:\/\/valgrind.org\/"},{"issue":"2","key":"256_CR52","first-page":"203","volume":"10","author":"W Visser","year":"2003","unstructured":"Visser, W., Havelund, K., Brat, G., Park, S.J., Lerda, F.: Model checking programs. FMSD 10(2), 203\u2013232 (2003)","journal-title":"FMSD"},{"key":"256_CR53","unstructured":"Weiser, M.: Program slicing. In: ICSE \u201981, pp. 439\u2013449. IEEE (1981)"},{"key":"256_CR54","doi-asserted-by":"crossref","unstructured":"Wilhelm, R., Sagiv, M., Reps, T.: Shape analysis. In: CC \u201900. LNCS, vol. 1781, pp. 1\u201316. Springer, Berlin (2000)","DOI":"10.1007\/3-540-46423-9_1"},{"key":"256_CR55","doi-asserted-by":"crossref","unstructured":"Xie, Y., Aiken, A.: SATURN: a scalable framework for error detection using boolean satisfiability. ACM TOPLAS 29(3), 16 (2007)","DOI":"10.1145\/1232420.1232423"},{"key":"256_CR56","doi-asserted-by":"crossref","unstructured":"Yu, D., Shao, Z.: Verification of safety properties for concurrent assembly code. In: ICFP \u201904, pp. 175\u2013188. ACM, New York (2004)","DOI":"10.1145\/1016850.1016875"},{"key":"256_CR57","doi-asserted-by":"crossref","first-page":"366","DOI":"10.1145\/267580.267590","volume":"29","author":"H Zhu","year":"1997","unstructured":"Zhu, H., Hall, P.A.V., May, J.H.R.: Software unit test coverage and adequacy. ACM Comput. Surv. 29, 366\u2013427 (1997)","journal-title":"ACM Comput. Surv."},{"issue":"6","key":"256_CR58","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1145\/1041685.1029911","volume":"29","author":"M Zitser","year":"2004","unstructured":"Zitser, M., Lippmann, R., Leek, T.: Testing static analysis tools using exploitable buffer overflows from open source code. SIGSOFT Softw. Eng. Notes 29(6), 97\u2013106 (2004)","journal-title":"SIGSOFT Softw. Eng. Notes"}],"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-012-0256-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-012-0256-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-012-0256-8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,6]],"date-time":"2025-04-06T14:31:41Z","timestamp":1743949901000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-012-0256-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,8,4]]},"references-count":58,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2014,2]]}},"alternative-id":["256"],"URL":"https:\/\/doi.org\/10.1007\/s10009-012-0256-8","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"type":"print","value":"1433-2779"},{"type":"electronic","value":"1433-2787"}],"subject":[],"published":{"date-parts":[[2012,8,4]]}}}