{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,13]],"date-time":"2026-02-13T10:17:11Z","timestamp":1770977831105,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540272311","type":"print"},{"value":"9783540316862","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11513988_17","type":"book-chapter","created":{"date-parts":[[2010,3,12]],"date-time":"2010-03-12T13:33:28Z","timestamp":1268400808000},"page":"158-163","source":"Crossref","is-referenced-by-count":33,"title":["Model Checking x86 Executables with CodeSurfer\/x86 and WPDS++"],"prefix":"10.1007","author":[{"given":"G.","family":"Balakrishnan","sequence":"first","affiliation":[]},{"given":"T.","family":"Reps","sequence":"additional","affiliation":[]},{"given":"N.","family":"Kidd","sequence":"additional","affiliation":[]},{"given":"A.","family":"Lal","sequence":"additional","affiliation":[]},{"given":"J.","family":"Lim","sequence":"additional","affiliation":[]},{"given":"D.","family":"Melski","sequence":"additional","affiliation":[]},{"given":"R.","family":"Gruian","sequence":"additional","affiliation":[]},{"given":"S.","family":"Yong","sequence":"additional","affiliation":[]},{"given":"C. -H.","family":"Chen","sequence":"additional","affiliation":[]},{"given":"T.","family":"Teitelbaum","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"17_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/978-3-540-24723-4_2","volume-title":"Compiler Construction","author":"G. Balakrishnan","year":"2004","unstructured":"Balakrishnan, G., Reps, T.: Analyzing memory accesses in x86 executables. In: Duesterwald, E. (ed.) CC 2004. LNCS, vol.\u00a02985, pp. 5\u201323. Springer, Heidelberg (2004)"},{"key":"17_CR2","unstructured":"Chen, H., Dean, D., Wagner, D.: Model checking one million lines of C code. In: Symp. on Network and Distributed Systems Security (2004)"},{"key":"17_CR3","unstructured":"Christodorescu, M., Jha, S.: Static analysis of executables to detect malicious patterns. In: USENIX Security Symposium (2003)"},{"key":"17_CR4","unstructured":"CodeSurfer, GrammaTech., Inc., http:\/\/www.grammatech.com\/products\/codesurfer\/"},{"key":"17_CR5","doi-asserted-by":"crossref","unstructured":"Dwyer, M., Avrunin, G., Corbett, J.: Patterns in property specifications for finite-state verification. In: Int. Conf. on Softw. Eng. (1999)","DOI":"10.1145\/302405.302672"},{"key":"17_CR6","unstructured":"Fast library identification and recognition technology, DataRescue sa\/nv, Li\u00e8ge, Belgium, http:\/\/www.datarescue.com\/idabase\/flirt.htm"},{"key":"17_CR7","first-page":"174","volume-title":"Princ. of Prog. Lang.","author":"P. Godefroid","year":"1997","unstructured":"Godefroid, P.: Model checking for programming languages using VeriSoft. In: ACM (ed.) Princ. of Prog. Lang., pp. 174\u2013186. ACM Press, New York (1997)"},{"key":"17_CR8","unstructured":"IDAPro disassembler, http:\/\/www.datarescue.com\/idabase\/"},{"key":"17_CR9","unstructured":"Kidd, N., Reps, T., Melski, D., Lal, A.: WPDS++: A C++ library for weighted pushdown systems. Univ. of Wisconsin (2004)"},{"key":"17_CR10","doi-asserted-by":"crossref","unstructured":"Lal, A., Reps, T., Balakrishnan, G.: Extended weighted pushdown systems. In: Computer Aided Verif. (2005)","DOI":"10.1007\/11513988_44"},{"key":"17_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/978-3-540-24732-6_4","volume-title":"Model Checking Software","author":"P. Leven","year":"2004","unstructured":"Leven, P., Mehler, T., Edelkamp, S.: Directed error detection in C++ with the assembly-level model checker StEAM. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol.\u00a02989, pp. 39\u201356. Springer, Heidelberg (2004)"},{"key":"17_CR12","doi-asserted-by":"crossref","unstructured":"M\u00fcller-Olm, M., Seidl, H.: Analysis of modular arithmetic. In: ESOP (2005)","DOI":"10.1007\/978-3-540-31987-0_5"},{"key":"17_CR13","doi-asserted-by":"crossref","unstructured":"Musuvathi, M., Park, D., Chou, A., Engler, D., Dill, D.: CMC: A pragmatic approach to model checking real code. In: Op. Syst. Design and Impl. (2002)","DOI":"10.1145\/1060289.1060297"},{"key":"17_CR14","doi-asserted-by":"crossref","unstructured":"Reps, T., Schwoon, S., Jha, S., Melski, D.: Weighted pushdown systems and their application to interprocedural dataflow analysis. Sci. of Comp. Prog. (2005) (To appear)","DOI":"10.1016\/j.scico.2005.02.009"},{"key":"17_CR15","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1016\/0304-3975(96)00072-2","volume":"167","author":"M. Sagiv","year":"1996","unstructured":"Sagiv, M., Reps, T., Horwitz, S.: Precise interprocedural dataflow analysis with applications to constant propagation. Theor. Comp. Sci.\u00a0167, 131\u2013170 (1996)","journal-title":"Theor. Comp. Sci."},{"key":"17_CR16","volume-title":"Program Flow Analysis: Theory and Applications","author":"M. Sharir","year":"1981","unstructured":"Sharir, M., Pnueli, A.: Two approaches to interprocedural data flow analysis. In: Program Flow Analysis: Theory and Applications. Prentice-Hall, Englewood Cliffs (1981)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11513988_17.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:05:00Z","timestamp":1605643500000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11513988_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540272311","9783540316862"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/11513988_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005]]}}}