{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T00:00:32Z","timestamp":1725753632833},"publisher-location":"Cham","reference-count":20,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319030760"},{"type":"electronic","value":"9783319030777"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-319-03077-7_20","type":"book-chapter","created":{"date-parts":[[2013,10,27]],"date-time":"2013-10-27T21:40:21Z","timestamp":1382910021000},"page":"295-310","source":"Crossref","is-referenced-by-count":3,"title":["Lazy Symbolic Execution through Abstraction and Sub-space Search"],"prefix":"10.1007","author":[{"given":"Guodong","family":"Li","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Indradeep","family":"Ghosh","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"20_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":"20_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/978-3-642-00768-2_27","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"N. Bj\u00f8rner","year":"2009","unstructured":"Bj\u00f8rner, N., Tillmann, N., Voronkov, A.: Path feasibility analysis for string-manipulating programs. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol.\u00a05505, pp. 307\u2013321. Springer, Heidelberg (2009)"},{"key":"20_CR3","doi-asserted-by":"crossref","unstructured":"Blanc, N., Groce, A., Kroening, D.: Verifying C++ with STL containers via predicate abstraction. In: Automated Software Engineering, ASE (2007)","DOI":"10.1145\/1321631.1321724"},{"key":"20_CR4","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":"20_CR5","unstructured":"Cadar, C., Dunbar, D., Engler, D.R.: KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In: Operating Systems Design and Implementation (OSDI) (2008)"},{"key":"20_CR6","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: Conference on Computer and Communications Security, CCS (2006)","DOI":"10.1145\/1180405.1180445"},{"key":"20_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-22110-1_1","volume-title":"Computer Aided Verification","author":"V. Ganesh","year":"2011","unstructured":"Ganesh, V., Kie\u017cun, A., Artzi, S., Guo, P.J., Hooimeijer, P., Ernst, M.: HAMPI: A string solver for testing, analysis and vulnerability detection. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 1\u201319. Springer, Heidelberg (2011)"},{"key":"20_CR8","doi-asserted-by":"crossref","unstructured":"Ghosh, I., Shafiei, N., Li, G., Chiang, W.-F.: JST: An automatic test generation tool for industrial java applications with strings. In: International Conference on Software Engineering, ICSE (2013)","DOI":"10.1109\/ICSE.2013.6606649"},{"key":"20_CR9","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Nori, A.V., Rajamani, S.K., Tetali, S.: Compositional may-must program analysis: unleashing the power of alternation. In: Symposium on Principles of Programming Languages, POPL (2010)","DOI":"10.1145\/1706299.1706307"},{"key":"20_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"553","DOI":"10.1007\/3-540-36577-X_40","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Khurshid","year":"2003","unstructured":"Khurshid, S., P\u0103s\u0103reanu, C.S., Visser, W.: Generalized symbolic execution for model checking and testing. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 553\u2013568. Springer, Heidelberg (2003)"},{"key":"20_CR11","doi-asserted-by":"crossref","unstructured":"Kuznetsov, V., Kinder, J., Bucur, S., Candea, G.: Efficient state merging in symbolic execution. In: Programming Language Design and Implementation (PLDI) (2012)","DOI":"10.1145\/2254064.2254088"},{"key":"20_CR12","unstructured":"Lattner, C., Adve, V.S.: LLVM: A compilation framework for lifelong program analysis & transformation. In: Symposium on Code Generation and Optimization (CGO) (2004)"},{"key":"20_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/978-3-642-21437-0_15","volume-title":"FM 2011: Formal Methods","author":"G. Li","year":"2011","unstructured":"Li, G.: Validated compilation through logic. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol.\u00a06664, pp. 169\u2013183. Springer, Heidelberg (2011)"},{"key":"20_CR14","series-title":"LNCS","first-page":"15","volume-title":"HVC 2013","author":"G. Li","year":"2013","unstructured":"Li, G., Ghosh, I.: PASS: String solving with parameterized array and interval automaton. In: Bertacco, V., Legay, A. (eds.) HVC 2013. LNCS, vol.\u00a08244, pp. 15\u201331. Springer, Heidelberg (2013)"},{"key":"20_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"609","DOI":"10.1007\/978-3-642-22110-1_49","volume-title":"Computer Aided Verification","author":"G. Li","year":"2011","unstructured":"Li, G., Ghosh, I., Rajan, S.P.: KLOVER: A symbolic execution and automatic test generation tool for C++ programs. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 609\u2013615. Springer, Heidelberg (2011)"},{"key":"20_CR16","doi-asserted-by":"crossref","unstructured":"Li, G., Li, P., Sawaga, G., Gopalakrishnan, G., Ghosh, I., Rajan, S.P.: GKLEE: Concolic verification and test generation for GPUs. In: Symposium on Principles and Practice of Parallel Programming (PPoPP) (2012)","DOI":"10.1145\/2145816.2145844"},{"issue":"2","key":"20_CR17","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1049\/iet-sen.2010.0029","volume":"5","author":"M. Lin","year":"2011","unstructured":"Lin, M., Li Chen, Y., Yu, K., Shi Wu, G.: Lazy symbolic execution for test data generation. IET Software\u00a05(2), 132\u2013141 (2011)","journal-title":"IET Software"},{"key":"20_CR18","unstructured":"Majumdar, R., Sen, K.: LATEST: Lazy dynamic test input generation. Tech. Rep. UCB\/EECS-2007, EECS Department, University of California, Berkeley (2007)"},{"key":"20_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/978-3-540-79124-9_10","volume-title":"Tests and Proofs","author":"N. Tillmann","year":"2008","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)"},{"key":"20_CR20","unstructured":"uClibc++: An embedded C++ library, \n                    \n                      http:\/\/cxx.uclibc.org"}],"container-title":["Lecture Notes in Computer Science","Hardware and Software: Verification and Testing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-03077-7_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,23]],"date-time":"2019-05-23T19:55:41Z","timestamp":1558641341000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-03077-7_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783319030760","9783319030777"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-03077-7_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}