{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T16:49:41Z","timestamp":1725814181108},"publisher-location":"Berlin, Heidelberg","reference-count":37,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662460801"},{"type":"electronic","value":"9783662460818"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-46081-8_21","type":"book-chapter","created":{"date-parts":[[2014,12,11]],"date-time":"2014-12-11T04:25:44Z","timestamp":1418271944000},"page":"373-392","source":"Crossref","is-referenced-by-count":9,"title":["Proving Memory Safety of the ANI Windows Image Parser Using Compositional Exhaustive Testing"],"prefix":"10.1007","author":[{"given":"Maria","family":"Christakis","sequence":"first","affiliation":[]},{"given":"Patrice","family":"Godefroid","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"21_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1007\/978-3-540-78800-3_28","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Anand","year":"2008","unstructured":"Anand, S., Godefroid, P., Tillmann, N.: Demand-driven compositional symbolic execution. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 367\u2013381. Springer, Heidelberg (2008)"},{"key":"21_CR2","doi-asserted-by":"publisher","first-page":"474","DOI":"10.1109\/TSE.2010.31","volume":"36","author":"S. Artzi","year":"2010","unstructured":"Artzi, S., Kiezun, A., Dolby, J., Tip, F., Dig, D., Paradkar, A.M., Ernst, M.D.: Finding bugs in web applications using dynamic test generation and explicit-state model checking. TSE\u00a036, 474\u2013494 (2010)","journal-title":"TSE"},{"key":"21_CR3","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.K.: The SLAM toolkit. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 260\u2013264. Springer, Heidelberg (2001)"},{"key":"21_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11804192_17","volume-title":"Formal Methods for Components and Objects","author":"M. Barnett","year":"2006","unstructured":"Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: A modular reusable verifier for object-oriented programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol.\u00a04111, pp. 364\u2013387. Springer, Heidelberg (2006)"},{"key":"21_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1007\/978-3-540-78800-3_27","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P. Boonstoppel","year":"2008","unstructured":"Boonstoppel, P., Cadar, C., Engler, D.: RWset: Attacking path explosion in constraint-based test generation. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 351\u2013366. Springer, Heidelberg (2008)"},{"key":"21_CR6","doi-asserted-by":"crossref","unstructured":"Bounimova, E., Godefroid, P., Molnar, D.A.: Billions and billions of constraints: Whitebox fuzz testing in production. In: ICSE, pp. 122\u2013131. ACM (2013)","DOI":"10.1109\/ICSE.2013.6606558"},{"key":"21_CR7","first-page":"775","volume":"30","author":"W.R. Bush","year":"2000","unstructured":"Bush, W.R., Pincus, J.D., Sielaff, D.J.: A static analyzer for finding dynamic programming errors. SPE\u00a030, 775\u2013802 (2000)","journal-title":"SPE"},{"key":"21_CR8","unstructured":"Cadar, C., Dunbar, D., Engler, D.R.: KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In: OSDI, pp. 209\u2013224. USENIX (2008)"},{"key":"21_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/11537328_2","volume-title":"Model Checking Software","author":"C. Cadar","year":"2005","unstructured":"Cadar, C., Engler, D.: Execution generated test cases: How to make systems code crash itself. In: Godefroid, P. (ed.) SPIN 2005. LNCS, vol.\u00a03639, pp. 2\u201323. Springer, Heidelberg (2005)"},{"key":"21_CR10","doi-asserted-by":"crossref","unstructured":"Cadar, C., Ganesh, V., Pawlowski, P.M., Dill, D.L., Engler, D.R.: EXE: Automatically generating inputs of death. In: CCS, pp. 322\u2013335. ACM (2006)","DOI":"10.1145\/1180405.1180445"},{"key":"21_CR11","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Kroening, D., Yorav, K.: Behavioral consistency of C and Verilog programs using bounded model checking. In: DAC, pp. 368\u2013371. ACM (2003)","DOI":"10.21236\/ADA461052"},{"key":"21_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-642-03359-9_2","volume-title":"Theorem Proving in Higher Order Logics","author":"E. Cohen","year":"2009","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: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 23\u201342. Springer, Heidelberg (2009)"},{"key":"21_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.S.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"21_CR14","doi-asserted-by":"crossref","unstructured":"Elkarablieh, B., Godefroid, P., Levin, M.Y.: Precise pointer reasoning for dynamic test generation. In: ISSTA, pp. 129\u2013140. ACM (2009)","DOI":"10.1145\/1572272.1572288"},{"key":"21_CR15","doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Compositional dynamic test generation. In: POPL, pp. 47\u201354. ACM (2007)","DOI":"10.1145\/1190215.1190226"},{"key":"21_CR16","doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Micro execution. In: ICSE, pp. 539\u2013549. ACM (2014)","DOI":"10.1145\/2568225.2568273"},{"key":"21_CR17","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Kinder, J.: Proving memory safety of floating-point computations by combining static and dynamic program analysis. In: ISSTA, pp. 1\u201312. ACM (2010)","DOI":"10.1145\/1831708.1831710"},{"key":"21_CR18","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Klarlund, N., Sen, K.: DART: Directed automated random testing. In: PLDI, pp. 213\u2013223. ACM (2005)","DOI":"10.1145\/1064978.1065036"},{"key":"21_CR19","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Lahiri, S.K., Rubio-Gonz\u00e1lez, C.: Statically validating must summaries for incremental compositional dynamic test generation. In: Yahav, E. (ed.) SAS 2011. LNCS, vol.\u00a06887, pp. 112\u2013128. Springer, Heidelberg (2011)","DOI":"10.1007\/978-3-642-23702-7_12"},{"key":"21_CR20","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Levin, M.Y., Molnar, D.A.: Active property checking. In: EMSOFT, pp. 207\u2013216. ACM (2008)","DOI":"10.1145\/1450058.1450087"},{"key":"21_CR21","unstructured":"Godefroid, P., Levin, M.Y., Molnar, D.A.: Automated whitebox fuzz testing. In: NDSS, pp. 151\u2013166. The Internet Society (2008)"},{"key":"21_CR22","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Luchaup, D.: Automatic partial loop summarization in dynamic test generation. In: ISSTA, pp. 23\u201333. ACM (2011)","DOI":"10.1145\/2001420.2001424"},{"key":"21_CR23","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL, pp. 58\u201370. ACM (2002)","DOI":"10.1145\/565816.503279"},{"key":"21_CR24","unstructured":"Howard, M.: Lessons learned from the animated cursor security bug (2007), \n                  \n                    http:\/\/blogs.msdn.com\/b\/sdl\/archive\/2007\/04\/26\/lessons-learned-from-the-animated-cursor-security-bug.aspx"},{"key":"21_CR25","doi-asserted-by":"crossref","unstructured":"Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: seL4: Formal verification of an OS kernel. In: SOSP, pp. 207\u2013220. ACM (2009)","DOI":"10.1145\/1629575.1629596"},{"key":"21_CR26","doi-asserted-by":"crossref","unstructured":"Kuznetsov, V., Kinder, J., Bucur, S., Candea, G.: Efficient state merging in symbolic execution. In: PLDI, pp. 193\u2013204. ACM (2012)","DOI":"10.1145\/2345156.2254088"},{"key":"21_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"806","DOI":"10.1007\/978-3-642-05089-3_51","volume-title":"FM 2009: Formal Methods","author":"D. Leinenbach","year":"2009","unstructured":"Leinenbach, D., Santen, T.: Verifying the Microsoft Hyper-V hypervisor with VCC. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol.\u00a05850, pp. 806\u2013809. Springer, Heidelberg (2009)"},{"key":"21_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"555","DOI":"10.1007\/978-3-642-02658-4_41","volume-title":"Computer Aided Verification","author":"R. Majumdar","year":"2009","unstructured":"Majumdar, R., Xu, R.-G.: Reducing test inputs using information partitions. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 555\u2013569. Springer, Heidelberg (2009)"},{"key":"21_CR29","doi-asserted-by":"crossref","unstructured":"Morrisett, J.G., Walker, D., Crary, K., Glew, N.: From system F to typed assembly language. In: POPL, pp. 85\u201397. ACM (1998)","DOI":"10.21236\/ADA358572"},{"key":"21_CR30","doi-asserted-by":"crossref","unstructured":"Necula, G.C., McPeak, S., Weimer, W.: CCured: Type-safe retrofitting of legacy code. In: POPL, pp. 128\u2013139. ACM (2002)","DOI":"10.1145\/565816.503286"},{"key":"21_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL\u2014A proof assistant for higher-order logic","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"21_CR32","doi-asserted-by":"crossref","unstructured":"Nori, A.V., Rajamani, S.K.: An empirical study of optimizations in YOGI. In: ICSE, pp. 355\u2013364. ACM (2010)","DOI":"10.1145\/1806799.1806852"},{"key":"21_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"419","DOI":"10.1007\/11817963_38","volume-title":"Computer Aided Verification","author":"K. Sen","year":"2006","unstructured":"Sen, K., Agha, G.: CUTE and jCUTE: Concolic unit testing and explicit path model-checking tools. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 419\u2013423. Springer, Heidelberg (2006)"},{"key":"21_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-89862-7_1","volume-title":"Information Systems Security","author":"D. Song","year":"2008","unstructured":"Song, D., et al.: BitBlaze: A new approach to computer security via binary analysis. In: Sekar, R., Pujari, A.K. (eds.) ICISS 2008. LNCS, vol.\u00a05352, pp. 1\u201325. Springer, Heidelberg (2008)"},{"key":"21_CR35","unstructured":"Sotirov, A.: Windows animated cursor stack overflow vulnerability (2007), \n                  \n                    http:\/\/www.offensive-security.com\/os101\/ani.htm"},{"key":"21_CR36","doi-asserted-by":"crossref","unstructured":"Tillmann, N., de Halleux, J.: Pex\u2013White Box Test Generation for .NET. In: Beckert, B., H\u00e4hnle, R. (eds.) TAP 2008. LNCS, vol.\u00a04966, pp. 134\u2013153. Springer, Heidelberg (2008)","DOI":"10.1007\/978-3-540-79124-9_10"},{"key":"21_CR37","doi-asserted-by":"crossref","unstructured":"Yang, J., Hawblitzel, C.: Safe to the last instruction: Automated verification of a type-safe operating system. In: PLDI, pp. 99\u2013110. ACM (2010)","DOI":"10.1145\/1809028.1806610"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-46081-8_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,28]],"date-time":"2019-05-28T20:34:36Z","timestamp":1559075676000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-46081-8_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662460801","9783662460818"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-46081-8_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}