{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:13:07Z","timestamp":1763467987528},"publisher-location":"Berlin, Heidelberg","reference-count":25,"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_27","type":"book-chapter","created":{"date-parts":[[2010,7,8]],"date-time":"2010-07-08T18:36:09Z","timestamp":1278614169000},"page":"288-305","source":"Crossref","is-referenced-by-count":36,"title":["Directed Proof Generation for Machine Code"],"prefix":"10.1007","author":[{"given":"Aditya","family":"Thakur","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Junghee","family":"Lim","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Akash","family":"Lal","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Amanda","family":"Burton","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Evan","family":"Driscoll","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Matt","family":"Elder","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tycho","family":"Andersen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Reps","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"27_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1007\/978-3-540-76336-9_3","volume-title":"Implementation and Application of Automata","author":"C. Allauzen","year":"2007","unstructured":"Allauzen, C., Riley, M., Schalkwyk, J., Skut, W., Mohri, M.: OpenFst: A general and efficient weighted finite-state transducer library. In: Holub, J., \u017d\u010f\u00e1rek, J. (eds.) CIAA 2007. LNCS, vol.\u00a04783, pp. 11\u201323. Springer, Heidelberg (2007)"},{"key":"27_CR2","doi-asserted-by":"crossref","unstructured":"Alur, R., Madhusudan, P.: Adding nesting structure to words. JACM\u00a056 (2009)","DOI":"10.1145\/1516512.1516518"},{"key":"27_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1007\/978-3-540-78800-3_10","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G. Balakrishnan","year":"2008","unstructured":"Balakrishnan, G., Reps, T.: Analyzing stripped device-driver executables. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 124\u2013140. Springer, Heidelberg (2008)"},{"key":"27_CR4","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":"27_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/3-540-44585-4_25","volume-title":"Computer Aided Verification","author":"T. Ball","year":"2001","unstructured":"Ball, T., Rajamani, S.: The SLAM toolkit. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, p. 260. Springer, Heidelberg (2001)"},{"key":"27_CR6","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":"27_CR7","volume-title":"Botnet Detection","author":"D. Brumley","year":"2008","unstructured":"Brumley, D., Hartwig, C., Liang, Z., Newsome, J., Poosankam, P., Song, D., Yin, H.: Automatically identifying trigger-based behavior in malware. In: Botnet Detection. Springer, Heidelberg (2008)"},{"key":"27_CR8","series-title":"Lecture Notes in Computer Science","volume-title":"Advances in Computer Systems Architecture","author":"M. Cova","year":"2006","unstructured":"Cova, M., Felmetsger, V., Banks, G., Vigna, G.: Static detection of vulnerabilities in x86 executables. In: Jesshope, C., Egan, C. (eds.) ACSAC 2006. LNCS, vol.\u00a04186. Springer, Heidelberg (2006)"},{"key":"27_CR9","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 (2007)","DOI":"10.1016\/j.scico.2007.01.015"},{"key":"27_CR10","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":"27_CR11","unstructured":"Godefroid, P., Levin, M., Molnar, D.: Automated whitebox fuzz testing. In: NDSS (2008)"},{"key":"27_CR12","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":"27_CR13","series-title":"Lecture Notes in Computer Science","first-page":"117","volume-title":"Fast Software Encryption","author":"B. Gulavani","year":"2006","unstructured":"Gulavani, B., Henzinger, T., Kannan, Y., Nori, A., Rajamani, S.: SYNERGY: A new algorithm for property checking. In: Robshaw, M.J.B. (ed.) FSE 2006. LNCS, vol.\u00a04047, pp. 117\u2013127. Springer, Heidelberg (2006)"},{"key":"27_CR14","doi-asserted-by":"crossref","unstructured":"Heizmann, M., Hoenicke, J., Podelski, A.: Nested interpolants. In: POPL (2010)","DOI":"10.1145\/1706299.1706353"},{"key":"27_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":"27_CR16","unstructured":"Kidd, N., Lal, A., Reps, T.: WALi: The Weighted Automaton Library (2007), http:\/\/www.cs.wisc.edu\/wpis\/wpds\/download.php"},{"key":"27_CR17","unstructured":"Kruegel, C., Kirda, E., Mutz, D., Robertson, W., Vigna, G.: Automating mimicry attacks using static binary analysis. In: USENIX Sec. Symp. (2005)"},{"key":"27_CR18","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":"27_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/978-3-540-78791-4_3","volume-title":"Compiler Construction","author":"J. Lim","year":"2008","unstructured":"Lim, J., Reps, T.: A system for generating static analyzers for machine instructions. In: Hendren, L. (ed.) CC 2008. LNCS, vol.\u00a04959, pp. 36\u201352. Springer, Heidelberg (2008)"},{"key":"27_CR20","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":"27_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"46","DOI":"10.1007\/978-3-540-31987-0_5","volume-title":"Programming Languages and Systems","author":"M. M\u00fcller-Olm","year":"2005","unstructured":"M\u00fcller-Olm, M., Seidl, H.: Analysis of modular arithmetic. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol.\u00a03444, pp. 46\u201360. Springer, Heidelberg (2005)"},{"key":"27_CR22","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":"27_CR23","doi-asserted-by":"crossref","unstructured":"Reps, T., Balakrishnan, G., Lim, J.: Intermediate-representation recovery from low-level code. In: PEPM (2006)","DOI":"10.1145\/1111542.1111560"},{"key":"27_CR24","unstructured":"Srivastava, A., Edwards, A., Vo, H.: Vulcan: Binary transformation in a distributed environment. MSR-TR-2001-50, Microsoft Research (April 2001)"},{"key":"27_CR25","doi-asserted-by":"crossref","unstructured":"Thakur, A., Lim, J., Lal, A., Burton, A., Driscoll, E., Elder, M., Andersen, T., Reps, T.: Directed proof generation for machine code. TR 1669, UW-Madison (April 2010)","DOI":"10.1007\/978-3-642-14295-6_27"}],"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_27.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,23]],"date-time":"2020-11-23T21:50:38Z","timestamp":1606168238000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14295-6_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642142949","9783642142956"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14295-6_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}