{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T17:56:07Z","timestamp":1725558967725},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642142949"},{"type":"electronic","value":"9783642142956"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-14295-6_6","type":"book-chapter","created":{"date-parts":[[2010,7,8]],"date-time":"2010-07-08T22:36:09Z","timestamp":1278628569000},"page":"41-56","source":"Crossref","is-referenced-by-count":15,"title":["There\u2019s Plenty of Room at the Bottom: Analyzing and Verifying Machine Code"],"prefix":"10.1007","author":[{"given":"Thomas","family":"Reps","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Junghee","family":"Lim","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Aditya","family":"Thakur","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gogul","family":"Balakrishnan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Akash","family":"Lal","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"6_CR1","doi-asserted-by":"crossref","unstructured":"Alur, R., Madhusudan, P.: Adding nesting structure to words. JACM\u00a056 (2009)","DOI":"10.1145\/1516512.1516518"},{"key":"6_CR2","doi-asserted-by":"crossref","unstructured":"Balakrishnan, G.: WYSINWYX: What You See Is Not What You eXecute. PhD thesis, C.S. Dept., Univ. of Wisconsin, Madison, WI, Tech. Rep. 1603 (August 2007)","DOI":"10.1007\/978-3-540-69149-5_22"},{"key":"6_CR3","unstructured":"Balakrishnan, G., Reps, T.: WYSINWYX: What You See Is Not What You eXecute. Trans. on Prog. Lang. and Syst. (to appear)"},{"key":"6_CR4","doi-asserted-by":"crossref","unstructured":"Balakrishnan, G., Reps, T.: Analyzing memory accesses in x86 executables. In: Comp. Construct., pp. 5\u201323 (2004)","DOI":"10.1007\/978-3-540-24723-4_2"},{"key":"6_CR5","doi-asserted-by":"crossref","unstructured":"Balakrishnan, G., Reps, T.: Recency-abstraction for heap-allocated storage. In: Static. Analysis Symp. (2006)","DOI":"10.1007\/11823230_15"},{"key":"6_CR6","unstructured":"Balakrishnan, G., Reps, T.: DIVINE: DIscovering Variables IN Executables. In: Verif., Model Checking, and Abs. Interp. (2007)"},{"key":"6_CR7","doi-asserted-by":"crossref","unstructured":"Balakrishnan, G., Reps, T.: Analyzing stripped device-driver executables. In: Tools and Algs. for the Construct. and Anal. of Syst. (2008)","DOI":"10.1007\/978-3-540-78800-3_10"},{"key":"6_CR8","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.\u00a03576, pp. 158\u2013163. Springer, Heidelberg (2005)"},{"key":"6_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/978-3-540-69149-5_22","volume-title":"Verified Software: Theories, Tools, Experiments","author":"G. Balakrishnan","year":"2008","unstructured":"Balakrishnan, G., Reps, T., Melski, D., Teitelbaum, T.: WYSINWYX: What You See Is Not What You eXecute. In: Meyer, B., Woodcock, J. (eds.) VSTTE 2005. LNCS, vol.\u00a04171, pp. 202\u2013213. Springer, Heidelberg (2008)"},{"key":"6_CR10","doi-asserted-by":"crossref","unstructured":"Beckman, N., Nori, A., Rajamani, S., Simmons, R.: Proofs from tests. In: Int. Symp. on Softw. Testing and Analysis (2008)","DOI":"10.1145\/1390630.1390634"},{"key":"6_CR11","doi-asserted-by":"crossref","unstructured":"Beyer, D., Henzinger, T., Majumdar, R., Rybalchenko, A.: Path invariants. In: Prog. Lang. Design and Impl. (2007)","DOI":"10.1145\/1250734.1250769"},{"key":"6_CR12","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction of approximation of fixed points. In: POPL (1977)","DOI":"10.1145\/512950.512973"},{"key":"6_CR13","doi-asserted-by":"crossref","unstructured":"Ernst, M., Perkins, J., Guo, P., McCamant, S., Pacheco, C., Tschantz, M., Xiao, C.: The Daikon system for dynamic detection of likely invariants. SCP\u00a069(1-3) (2007)","DOI":"10.1016\/j.scico.2007.01.015"},{"key":"6_CR14","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Klarlund, N., Sen, K.: DART: Directed automated random testing. In: Prog. Lang. Design and Impl. (2005)","DOI":"10.1145\/1065010.1065036"},{"key":"6_CR15","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Nori, A., Rajamani, S., Tetali, S.: Compositional may-must program analysis: Unleashing the power of alternation. In: POPL (2010)","DOI":"10.1145\/1706299.1706307"},{"key":"6_CR16","doi-asserted-by":"crossref","unstructured":"Gulavani, B., Henzinger, T., Kannan, Y., Nori, A., Rajamani, S.: SYNERGY: A new algorithm for property checking. In: Found. of Softw. Eng. (2006)","DOI":"10.1145\/1181775.1181790"},{"key":"6_CR17","doi-asserted-by":"crossref","unstructured":"Heizmann, M., Hoenicke, J., Podelski, A.: Nested interpolants. In: POPL (2010)","DOI":"10.1145\/1706299.1706353"},{"key":"6_CR18","unstructured":"Johnson, S.: YACC: Yet another compiler-compiler. Technical Report Comp. Sci. Tech. Rep. 32, Bell Laboratories (1975)"},{"key":"6_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"434","DOI":"10.1007\/11513988_44","volume-title":"Computer Aided Verification","author":"A. Lal","year":"2005","unstructured":"Lal, A., Reps, T., Balakrishnan, G.: Extended weighted pushdown systems. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 434\u2013448. Springer, Heidelberg (2005)"},{"key":"6_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/978-3-642-02652-2_14","volume-title":"Model Checking Software","author":"J. Lim","year":"2009","unstructured":"Lim, J., Lal, A., Reps, T.: Symbolic analysis via semantic reinterpretation. In: P\u0103s\u0103reanu, C.S. (ed.) SPIN Workshop. LNCS, vol.\u00a05578, pp. 148\u2013168. Springer, Heidelberg (2009)"},{"key":"6_CR21","doi-asserted-by":"crossref","unstructured":"Lim, J., Reps, T.: A system for generating static analyzers for machine instructions. In: Comp. Construct. (2008)","DOI":"10.1007\/978-3-540-78791-4_3"},{"key":"6_CR22","doi-asserted-by":"crossref","unstructured":"Linn, C., Debray, S.: Obfuscation of executable code to improve resistance to static disassembly. In: CCS (2003)","DOI":"10.1145\/948109.948149"},{"key":"6_CR23","doi-asserted-by":"crossref","unstructured":"M\u00fcller-Olm, M., Seidl, H.: Analysis of modular arithmetic. In: European Symp. on Programming (2005)","DOI":"10.1007\/978-3-540-31987-0_5"},{"key":"6_CR24","doi-asserted-by":"crossref","unstructured":"Ramalingam, G., Field, J., Tip, F.: Aggregate structure identification and its application to program analysis. In: POPL (1999)","DOI":"10.1145\/292540.292553"},{"key":"6_CR25","doi-asserted-by":"crossref","unstructured":"Reps, T., Balakrishnan, G., Lim, J.: Intermediate-representation recovery from low-level code. In: Part. Eval. and Semantics-Based Prog. Manip. (2006)","DOI":"10.1145\/1111542.1111560"},{"key":"6_CR26","doi-asserted-by":"crossref","unstructured":"Reps, T., Balakrishnan, G., Lim, J., Teitelbaum, T.: A next-generation platform for analyzing executables. In: Asian Symp. on Prog. Lang. and Systems (2005)","DOI":"10.1007\/11575467_15"},{"key":"6_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"288","DOI":"10.1007\/978-3-642-14295-6_27","volume-title":"CAV 2010","author":"A. Thakur","year":"2010","unstructured":"Thakur, A., Lim, J., Lal, A., Burton, A., Driscoll, E., Elder, M., Andersen, T., Reps, T.: Directed proof generation for machine code. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 288\u2013305. Springer, Heidelberg (2010)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-14295-6_6.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T02:50:42Z","timestamp":1606186242000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14295-6_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642142949","9783642142956"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14295-6_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}