{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:12:51Z","timestamp":1763467971876},"reference-count":37,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2010,5,15]],"date-time":"2010-05-15T00:00:00Z","timestamp":1273881600000},"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":[[2011,1]]},"DOI":"10.1007\/s10009-010-0158-6","type":"journal-article","created":{"date-parts":[[2010,5,13]],"date-time":"2010-05-13T22:28:43Z","timestamp":1273789723000},"page":"61-87","source":"Crossref","is-referenced-by-count":7,"title":["Symbolic analysis via semantic reinterpretation"],"prefix":"10.1007","volume":"13","author":[{"given":"Junghee","family":"Lim","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Akash","family":"Lal","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Reps","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2010,5,15]]},"reference":[{"key":"158_CR1","doi-asserted-by":"crossref","unstructured":"Ball, T., Majumdar, R., Millstein, T., Rajamani, S.: Automatic predicate abstraction of C programs. In: PLDI (2001)","DOI":"10.1145\/378795.378846"},{"key":"158_CR2","doi-asserted-by":"crossref","unstructured":"Barnett, M., Chang, B.-Y., DeLine, R., Jacobs, B., Leino, K.: Boogie: A modular reusable verifier for object-oriented programs. In: Formal Methods for Components and Objects (2005)","DOI":"10.1007\/11804192_17"},{"key":"158_CR3","doi-asserted-by":"crossref","unstructured":"Beckman, N., Nori, A., Rajamani, S., Simmons, R.: Proofs from tests. In: ISSTA (2008)","DOI":"10.1145\/1390630.1390634"},{"key":"158_CR4","doi-asserted-by":"crossref","unstructured":"Birkedal, L., Welinder, M.: Hand-writing program generator generators. In: PLILP (1994)","DOI":"10.1007\/3-540-58402-1_15"},{"key":"158_CR5","doi-asserted-by":"crossref","unstructured":"Brumley, D., Hartwig, C., Liang, Z., Newsome, J., Poosankam, P., Song, D., Yin, H.: Automatically identifying trigger-based behavior in malware. In: Botnet Analysis and Defense. Springer, Berlin (2008)","DOI":"10.1007\/978-0-387-68768-1_4"},{"key":"158_CR6","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation. In: POPL (1977)","DOI":"10.1145\/512950.512973"},{"key":"158_CR7","unstructured":"Coverity, Inc. Coverity Prevent. www.coverity.com\/html\/coverity-prevent.html"},{"key":"158_CR8","doi-asserted-by":"crossref","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Int. Conf. on Tools and Algs. for the Construction and Analysis of Systems (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"158_CR9","unstructured":"Dutertre, B., de Moura, L.: Yices: an SMT solver (2006). http:\/\/yices.csl.sri.com\/"},{"key":"158_CR10","unstructured":"Ganesh, V., Dill, D.: A decision procesure for bit-vectors and arrays. In: CAV (2007)"},{"key":"158_CR11","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Klarlund, N., Sen, K.: DART: Directed automated random testing. In: PLDI (2005)","DOI":"10.1145\/1065010.1065036"},{"key":"158_CR12","unstructured":"Godefroid, P., Levin, M., Molnar, D.: Automated whitebox fuzz testing. In: NDSS (2008)"},{"key":"158_CR13","unstructured":"GrammaTech, Inc. CodeSonar. http:\/\/www.grammatech.com\/products\/codesonar"},{"key":"158_CR14","doi-asserted-by":"crossref","unstructured":"Gulavani, B., Henzinger, T., Kannan, Y., Nori, A., Rajamani, S.: SYNERGY: a new algorithm for property checking. In: FSE (2006)","DOI":"10.1145\/1181775.1181790"},{"key":"158_CR15","doi-asserted-by":"crossref","unstructured":"Henzinger, T., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL (2002)","DOI":"10.1145\/503272.503279"},{"key":"158_CR16","unstructured":"Intel.: Intel 64 and IA-32 Architectures Software Developer\u2019s Manual, vol. 2A: Instruction Set Reference, A-M. http:\/\/download.intel.com\/design\/processor\/manuals\/253666.pdf"},{"key":"158_CR17","unstructured":"Intel.: Intel 64 and IA-32 Architectures Software Developer\u2019s Manual, vol. 2B: Instruction Set Reference, N-Z. http:\/\/download.intel.com\/design\/processor\/manuals\/253667.pdf"},{"key":"158_CR18","unstructured":"Jhala, R., Majumdar, R.: B2: Software model checking for C (2009). http:\/\/www.cs.ucla.edu\/~rupak\/b2\/"},{"key":"158_CR19","volume-title":"Partial Evaluation and Automatic Program Generation","author":"N. Jones","year":"1993","unstructured":"Jones N., Gomard C., Sestoft P.: Partial Evaluation and Automatic Program Generation. Prentice-Hall, Englewood Cliffs (1993)"},{"key":"158_CR20","doi-asserted-by":"crossref","unstructured":"Jones, N., Mycroft, A.: Data flow analysis of applicative programs using minimal function graphs. In: POPL, pp. 296\u2013306 (1986)","DOI":"10.1145\/512644.512672"},{"key":"158_CR21","unstructured":"Lal, A., Lim, J., Reps, T.: McDash: Refinement-based property verification for machine code. TR-1649, Comp. Sci. Dept., Univ. of Wisconsin, Madison, WI (2009)"},{"key":"158_CR22","doi-asserted-by":"crossref","unstructured":"Lee, P., Leone, M.: Optimizing ML with run-time code generation. In: PLDI (1996)","DOI":"10.1145\/231379.231407"},{"key":"158_CR23","doi-asserted-by":"crossref","unstructured":"Lim, J., Lal, A., Reps, T.: Symbolic analysis via semantic reinterpretation. In: Spin Workshop (2009)","DOI":"10.1007\/978-3-642-02652-2_14"},{"key":"158_CR24","unstructured":"Lim, J., Reps, T.: A system for generating static analyzers for machine instructions. TR-1622, CS Dept., Univ. of Wisconsin, Madison, WI (2007)"},{"key":"158_CR25","doi-asserted-by":"crossref","unstructured":"Lim, J., Reps, T.: A system for generating static analyzers for machine instructions. In: CC (2008)","DOI":"10.1007\/978-3-540-78791-4_3"},{"key":"158_CR26","unstructured":"Malmkj\u00e6r, K.: Abstract interpretation of partial-evaluation algorithms. PhD thesis, Dept. of Comp. and Inf. Sci., Kansas State Univ. (1993)"},{"key":"158_CR27","volume-title":"Theor. Found. of Program. Methodology","author":"J. Morris","year":"1982","unstructured":"Morris J.: A general axiom of assignment. In: Broy, M., Schmidt, G. (eds) Theor. Found. of Program. Methodology, Reidel, Dordrecht (1982)"},{"key":"158_CR28","doi-asserted-by":"crossref","unstructured":"Mosses, P.: A semantic algebra for binding constructs. In: ICFPC (1981)","DOI":"10.1007\/3-540-10699-5_115"},{"key":"158_CR29","doi-asserted-by":"crossref","unstructured":"Mycroft, A., Jones, N.: A relational framework for abstract interpretation. In: PADO (1985)","DOI":"10.1007\/3-540-16446-4_9"},{"key":"158_CR30","doi-asserted-by":"crossref","unstructured":"Necula, G., Lee, P.: Safe kernel extensions without run-time checking. In: OSDI (1996)","DOI":"10.1145\/238721.238781"},{"key":"158_CR31","doi-asserted-by":"crossref","unstructured":"Nelson, G.: A generalization of Dijkstra\u2019s calculus. TOPLAS 11(4) (1989)","DOI":"10.1145\/69558.69559"},{"key":"158_CR32","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1016\/0304-3975(89)90091-1","volume":"69","author":"F. Nielson","year":"1989","unstructured":"Nielson F.: Two-level semantics and abstract interpretation. TCS 69, 117\u2013242 (1989)","journal-title":"TCS"},{"key":"158_CR33","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511526572","volume-title":"Two-Level Functional Languages","author":"F. Nielson","year":"1992","unstructured":"Nielson F., Nielson H.: Two-Level Functional Languages. Cambridge University Press, Cambridge (1992)"},{"key":"158_CR34","doi-asserted-by":"crossref","unstructured":"Sen, K., Marinov, D., Agha, G.: CUTE: a concolic unit testing engine for C. In: FSE (2005)","DOI":"10.1145\/1081706.1081750"},{"key":"158_CR35","doi-asserted-by":"crossref","first-page":"227","DOI":"10.1016\/0304-3975(82)90067-6","volume":"18","author":"J. Sifakis","year":"1982","unstructured":"Sifakis J.: A unified approach for studying the properties of transition systems. TCS 18, 227\u2013258 (1982)","journal-title":"TCS"},{"key":"158_CR36","doi-asserted-by":"crossref","unstructured":"Xie, Y., Aiken, A. (2007) Saturn: a scalable framework for error detection using Boolean satisfiability. TOPLAS 29(3)","DOI":"10.1145\/1232420.1232423"},{"key":"158_CR37","doi-asserted-by":"crossref","unstructured":"Xie, Y., Chou, A., Engler, D.: ARCHER: Using symbolic, path-sensitive analysis to detect memory access errors. In: FSE (2003)","DOI":"10.1145\/949952.940115"}],"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-010-0158-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-010-0158-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-010-0158-6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T07:25:26Z","timestamp":1559114726000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-010-0158-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,5,15]]},"references-count":37,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2011,1]]}},"alternative-id":["158"],"URL":"https:\/\/doi.org\/10.1007\/s10009-010-0158-6","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,5,15]]}}}