{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T21:01:13Z","timestamp":1751662873110,"version":"3.41.0"},"publisher-location":"Cham","reference-count":47,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319779348"},{"type":"electronic","value":"9783319779355"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-77935-5_28","type":"book-chapter","created":{"date-parts":[[2018,3,10]],"date-time":"2018-03-10T15:02:34Z","timestamp":1520694154000},"page":"416-434","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Using Test Ranges to Improve Symbolic Execution"],"prefix":"10.1007","author":[{"given":"Rui","family":"Qiu","sequence":"first","affiliation":[]},{"given":"Sarfraz","family":"Khurshid","sequence":"additional","affiliation":[]},{"given":"Corina S.","family":"P\u0103s\u0103reanu","sequence":"additional","affiliation":[]},{"given":"Junye","family":"Wen","sequence":"additional","affiliation":[]},{"given":"Guowei","family":"Yang","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,3,11]]},"reference":[{"key":"28_CR1","unstructured":"Stampede. https:\/\/www.tacc.utexas.edu\/stampede"},{"key":"28_CR2","unstructured":"http:\/\/cs.txstate.edu\/~g_y10\/synergise"},{"key":"28_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/978-3-642-20551-4_7","volume-title":"Logic-Based Program Synthesis and Transformation","author":"E Albert","year":"2011","unstructured":"Albert, E., G\u00f3mez-Zamalloa, M., Rojas, J.M., Puebla, G.: Compositional CLP-based test data generation for imperative languages. In: Alpuente, M. (ed.) LOPSTR 2010. LNCS, vol. 6564, pp. 99\u2013116. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-20551-4_7"},{"issue":"8","key":"28_CR4","doi-asserted-by":"crossref","first-page":"1978","DOI":"10.1016\/j.jss.2013.02.061","volume":"86","author":"S Anand","year":"2013","unstructured":"Anand, S., Burke, E.K., Chen, T.Y., Clark, J., Cohen, M.B., Grieskamp, W., Harman, M., Harrold, M.J., Mcminn, P.: An orchestrated survey of methodologies for automated software test case generation. J. Syst. Softw. 86(8), 1978\u20132001 (2013)","journal-title":"J. Syst. Softw."},{"key":"28_CR5","doi-asserted-by":"crossref","unstructured":"Baars, A.I., Harman, M., Hassoun, Y., Lakhotia, K., McMinn, P., Tonella, P., Vos, T.E.J.: Symbolic search-based testing. In: ASE 2011, pp. 53\u201362 (2011)","DOI":"10.1109\/ASE.2011.6100119"},{"key":"28_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/978-3-319-47166-2_14","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques","author":"D Beyer","year":"2016","unstructured":"Beyer, D., Lemberger, T.: Symbolic execution with CEGAR. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9952, pp. 195\u2013211. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-47166-2_14"},{"key":"28_CR7","doi-asserted-by":"crossref","unstructured":"Boyapati, C., Khurshid, S., Marinov, D.: Korat: automated testing based on Java predicates. In: ISSTA 2002, pp. 123\u2013133 (2002)","DOI":"10.1145\/566172.566191"},{"key":"28_CR8","doi-asserted-by":"crossref","unstructured":"Bucur, S., Ureche, V., Zamfir, C., Candea, G.: Parallel symbolic execution for automated real-world software testing. In: EuroSys 2011, pp. 183\u2013198 (2011)","DOI":"10.1145\/1966445.1966463"},{"key":"28_CR9","unstructured":"Cadar, C., Dunbar, D., Engler, D.R.: KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In: OSDI 2008, pp. 209\u2013224 (2008)"},{"key":"28_CR10","unstructured":"Chen, J., Hu, W., Zhang, L., Hao, D., Khurshid, S., Liu, X., Zhang, L.: Learning to accelerate symbolic execution via code transformation. Under peer-review"},{"key":"28_CR11","doi-asserted-by":"crossref","unstructured":"Clarke, L.A.: A program testing system. In: ACM 1976, pp. 488\u2013491 (1976)","DOI":"10.1145\/800191.805647"},{"key":"28_CR12","unstructured":"Dini, N.: MKorat: a novel approach for memorizing the Korat search and some potential applications. Master\u2019s thesis, University of Texas at Austin (2016)"},{"key":"28_CR13","doi-asserted-by":"crossref","unstructured":"Dong, S., Olivo, O., Zhang, L., Khurshid, S.: Studying the influence of standard compiler optimizations on symbolic execution. In: ISSRE 2015, pp. 205\u2013215 (2015)","DOI":"10.1109\/ISSRE.2015.7381814"},{"key":"28_CR14","unstructured":"Message Passing Interface Forum: MPI: a message-passing interface standard. Technical report, Knoxville, TN, USA (1994)"},{"key":"28_CR15","doi-asserted-by":"crossref","unstructured":"Fraser, G., Arcuri, A.: Evolutionary generation of whole test suites. In: QSIC 2011, Los Alamitos, CA, USA, pp. 31\u201340 (2011)","DOI":"10.1109\/QSIC.2011.19"},{"key":"28_CR16","doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Compositional dynamic test generation. In: POPL 2007, pp. 47\u201354 (2007)","DOI":"10.1145\/1190216.1190226"},{"key":"28_CR17","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Klarlund, N., Sen, K.: DART: directed automated random testing. In: PLDI 2005, pp. 213\u2013223 (2005)","DOI":"10.1145\/1065010.1065036"},{"key":"28_CR18","doi-asserted-by":"crossref","unstructured":"Inkumsah, K., Xie, T.: Evacon: a framework for integrating evolutionary and concolic testing for object-oriented programs. In: ASE 2007, pp. 425\u2013428 (2007)","DOI":"10.1145\/1321631.1321700"},{"key":"28_CR19","doi-asserted-by":"crossref","unstructured":"Inkumsah, K., Xie, T.: Improving structural testing of object-oriented programs via integrating evolutionary testing and symbolic execution. In: ASE 2008, pp. 297\u2013306 (2008)","DOI":"10.1109\/ASE.2008.40"},{"issue":"5","key":"28_CR20","doi-asserted-by":"crossref","first-page":"649","DOI":"10.1109\/TSE.2010.62","volume":"37","author":"Y Jia","year":"2011","unstructured":"Jia, Y., Harman, M.: An analysis and survey of the development of mutation testing. IEEE Trans. Softw. Eng. 37(5), 649\u2013678 (2011)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"28_CR21","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. 2619, pp. 553\u2013568. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-36577-X_40"},{"key":"28_CR22","doi-asserted-by":"crossref","unstructured":"Kim, M., Kim, Y., Rothermel, G.: A scalable distributed concolic testing approach: an empirical evaluation. In: ICST 2012, pp. 340\u2013349 (2012)","DOI":"10.1109\/ICST.2012.114"},{"issue":"7","key":"28_CR23","doi-asserted-by":"crossref","first-page":"385","DOI":"10.1145\/360248.360252","volume":"19","author":"JC King","year":"1976","unstructured":"King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385\u2013394 (1976)","journal-title":"Commun. ACM"},{"issue":"12","key":"28_CR24","doi-asserted-by":"crossref","first-page":"2379","DOI":"10.1016\/j.jss.2010.07.026","volume":"83","author":"K Lakhotia","year":"2010","unstructured":"Lakhotia, K., McMinn, P., Harman, M.: An empirical investigation into branch coverage for C programs using CUTE and AUSTIN. J. Syst. Softw. 83(12), 2379\u20132391 (2010)","journal-title":"J. Syst. Softw."},{"key":"28_CR25","doi-asserted-by":"crossref","unstructured":"Li, G., Andreasen, E., Ghosh, I.: SymJS: automatic symbolic testing of Javascript web applications. In: FSE 2014, pp. 449\u2013459 (2014)","DOI":"10.1145\/2635868.2635913"},{"key":"28_CR26","doi-asserted-by":"crossref","unstructured":"Liew, D., Cadar, C., Donaldson, A.F.: Symbooglix: a symbolic execution engine for boogie programs. In: ICST 2016, pp. 45\u201356 (2016)","DOI":"10.1109\/ICST.2016.11"},{"key":"28_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/978-3-642-23702-7_11","volume-title":"Static Analysis","author":"K-K Ma","year":"2011","unstructured":"Ma, K.-K., Yit Phang, K., Foster, J.S., Hicks, M.: Directed symbolic execution. In: Yahav, E. (ed.) SAS 2011. LNCS, vol. 6887, pp. 95\u2013111. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-23702-7_11"},{"key":"28_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"504","DOI":"10.1007\/11531142_22","volume-title":"ECOOP 2005 - Object-Oriented Programming","author":"C Pacheco","year":"2005","unstructured":"Pacheco, C., Ernst, M.D.: Eclat: automatic generation and classification of test inputs. In: Black, A.P. (ed.) ECOOP 2005. LNCS, vol. 3586, pp. 504\u2013527. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11531142_22"},{"key":"28_CR29","doi-asserted-by":"crossref","unstructured":"Pacheco, C., Lahiri, S.K., Ernst, M.D., Ball, T.: Feedback-directed random test generation. In: ICSE 2007, Minneapolis, MN, USA, 23\u201325 May 2007, pp. 75\u201384 (2007)","DOI":"10.1109\/ICSE.2007.37"},{"key":"28_CR30","doi-asserted-by":"crossref","unstructured":"Person, S., Yang, G., Rungta, N., Khurshid, S.: Directed incremental symbolic execution. In: PLDI 2011, pp. 504\u2013515 (2011)","DOI":"10.1145\/1993498.1993558"},{"key":"28_CR31","doi-asserted-by":"crossref","unstructured":"P\u0103s\u0103reanu, C.S., Mehlitz, P.C., Bushnell, D.H., Gundy-Burlet, K., Lowry, M., Person, S., Pape, M.: Combining unit-level symbolic execution and system-level concrete execution for testing NASA software. In: ISSTA 2008, pp. 15\u201325 (2008)","DOI":"10.1145\/1390630.1390635"},{"key":"28_CR32","doi-asserted-by":"crossref","unstructured":"P\u0103s\u0103reanu, C.S., Rungta, N.: Symbolic PathFinder: symbolic execution of Java bytecode. In: ASE 2010, pp. 179\u2013180 (2010)","DOI":"10.1145\/1858996.1859035"},{"key":"28_CR33","doi-asserted-by":"crossref","unstructured":"Qiu, R., Khurshid, S., P\u0103s\u0103reanu, C.S., Yang, G.: A synergistic approach for distributed symbolic execution using test ranges. In: ICSE 2017 - Companion, pp. 130\u2013132 (2017)","DOI":"10.1109\/ICSE-C.2017.116"},{"key":"28_CR34","doi-asserted-by":"crossref","unstructured":"Qiu, R., Yang, G., P\u0103s\u0103reanu, C.S., Khurshid, S.: Compositional symbolic execution with memoized replay. In: ICSE 2015, pp. 632\u2013642 (2015)","DOI":"10.1109\/ICSE.2015.79"},{"key":"28_CR35","unstructured":"Rojas, J.M., P\u0103s\u0103reanu, C.S.: Compositional symbolic execution through program specialization. In: BYTECODE 2013 (ETAPS) (2013)"},{"key":"28_CR36","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. 4144, pp. 419\u2013423. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11817963_38"},{"issue":"6","key":"28_CR37","doi-asserted-by":"crossref","first-page":"532","DOI":"10.1016\/j.jpdc.2009.02.006","volume":"69","author":"A Shafi","year":"2009","unstructured":"Shafi, A., Carpenter, B., Baker, M.: Nested parallelism for multi-core HPC systems using Java. J. Parallel Distrib. Comput. 69(6), 532\u2013545 (2009)","journal-title":"J. Parallel Distrib. Comput."},{"key":"28_CR38","doi-asserted-by":"crossref","unstructured":"Siddiqui, J.H., Khurshid, S.: ParSym: parallel symbolic execution. In: ICSTE 2010, vol. 1, pp. V1-405\u2013V1-409, October 2010","DOI":"10.1109\/ICSTE.2010.5608866"},{"key":"28_CR39","doi-asserted-by":"crossref","unstructured":"Siddiqui, J.H., Khurshid, S.: Scaling symbolic execution using ranged analysis. In: OOPSLA 2012, pp. 523\u2013536 (2012)","DOI":"10.1145\/2384616.2384654"},{"key":"28_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/978-3-642-32469-7_14","volume-title":"Formal Methods for Industrial Critical Systems","author":"J Slab\u00fd","year":"2012","unstructured":"Slab\u00fd, J., Strej\u010dek, J., Trt\u00edk, M.: Checking properties described by state machines: on synergy of instrumentation, slicing, and symbolic execution. In: Stoelinga, M., Pinger, R. (eds.) FMICS 2012. LNCS, vol. 7437, pp. 207\u2013221. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-32469-7_14"},{"key":"28_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/978-3-642-20398-5_26","volume-title":"NASA Formal Methods","author":"M Souza","year":"2011","unstructured":"Souza, M., Borges, M., d\u2019Amorim, M., P\u0103s\u0103reanu, C.S.: CORAL: solving complex constraints for symbolic pathfinder. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 359\u2013374. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-20398-5_26"},{"key":"28_CR42","doi-asserted-by":"crossref","unstructured":"Staats, M., P\u01ces\u01cereanu, C.: Parallel symbolic execution for structural test generation. In ISSTA 2010, pp. 183\u2013194 (2010)","DOI":"10.1145\/1831708.1831732"},{"key":"28_CR43","doi-asserted-by":"crossref","unstructured":"Visser, W., Geldenhuys, J., Dwyer, M.B.: Green: reducing, reusing and recycling constraints in program analysis. In: FSE 2012, pp. 58:1\u201358:11 (2012)","DOI":"10.1145\/2393596.2393665"},{"key":"28_CR44","unstructured":"Wang, R., Ning, P., Xie, T., Chen, Q.: MetaSymploit: day-one defense against script-based attacks with security-enhanced symbolic analysis. In: USENIX Security 2013, pp. 65\u201380 (2013)"},{"key":"28_CR45","doi-asserted-by":"crossref","unstructured":"Yang, G., Khurshid, S., Person, S., Rungta, N.: Property differencing for incremental checking. In: ICSE 2014, pp. 1059\u20131070 (2014)","DOI":"10.1145\/2568225.2568319"},{"key":"28_CR46","doi-asserted-by":"crossref","unstructured":"Yang, G., P\u0103s\u0103reanu, C.S., Khurshid, S.: Memoized symbolic execution. In ISSTA 2012, pp. 144\u2013154 (2012)","DOI":"10.1145\/2338965.2336771"},{"issue":"1","key":"28_CR47","doi-asserted-by":"crossref","first-page":"3:1","DOI":"10.1145\/2629536","volume":"24","author":"G Yang","year":"2014","unstructured":"Yang, G., Person, S., Rungta, N., Khurshid, S.: Directed incremental symbolic execution. ACM Trans. Softw. Eng. Methodol. 24(1), 3:1\u20133:42 (2014)","journal-title":"ACM Trans. Softw. Eng. Methodol."}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-77935-5_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,2]],"date-time":"2025-07-02T18:09:32Z","timestamp":1751479772000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-77935-5_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319779348","9783319779355"],"references-count":47,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-77935-5_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}