{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T18:52:52Z","timestamp":1777488772977,"version":"3.51.4"},"reference-count":78,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2013,2,26]],"date-time":"2013-02-26T00:00:00Z","timestamp":1361836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Autom Softw Eng"],"published-print":{"date-parts":[[2013,9]]},"DOI":"10.1007\/s10515-013-0122-2","type":"journal-article","created":{"date-parts":[[2013,2,25]],"date-time":"2013-02-25T16:01:31Z","timestamp":1361808091000},"page":"391-425","source":"Crossref","is-referenced-by-count":127,"title":["Symbolic PathFinder: integrating symbolic execution with model checking for Java bytecode analysis"],"prefix":"10.1007","volume":"20","author":[{"given":"Corina S.","family":"P\u0103s\u0103reanu","sequence":"first","affiliation":[]},{"given":"Willem","family":"Visser","sequence":"additional","affiliation":[]},{"given":"David","family":"Bushnell","sequence":"additional","affiliation":[]},{"given":"Jaco","family":"Geldenhuys","sequence":"additional","affiliation":[]},{"given":"Peter","family":"Mehlitz","sequence":"additional","affiliation":[]},{"given":"Neha","family":"Rungta","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2013,2,26]]},"reference":[{"key":"122_CR1","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/978-3-540-71209-1_12","volume-title":"Proc. 13th Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"S. Anand","year":"2007","unstructured":"Anand, S., P\u0103s\u0103reanu, C.S., Visser, W.: JPF\u2013SE: a symbolic execution extension to Java PathFinder. In: Proc. 13th Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 4424, pp. 134\u2013138. Springer, Berlin (2007)"},{"issue":"1","key":"122_CR2","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1007\/s10009-008-0090-1","volume":"11","author":"S. Anand","year":"2009","unstructured":"Anand, S., P\u0103s\u0103reanu, C.S., Visser, W.: Symbolic execution with abstraction. Int. J. Softw. Tools Technol. Transf. 11(1), 53\u201367 (2009)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"122_CR3","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1145\/2001420.2001427","volume-title":"Proc. 2011 International Symposium on Software Testing and Analysis (ISSTA)","author":"D. Balasubramanian","year":"2011","unstructured":"Balasubramanian, D., P\u0103s\u0103reanu, C.S., Whalen, M.W., Karsai, G., Lowry, M.R.: Polyglot: modeling and analysis for multiple statechart formalisms. In: Proc. 2011 International Symposium on Software Testing and Analysis (ISSTA), pp. 45\u201355 (2011)"},{"key":"122_CR4","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1007\/978-3-642-28891-3_26","volume-title":"Proc. NASA Formal Methods 2012","author":"D. Balasubramanian","year":"2012","unstructured":"Balasubramanian, D., P\u0103s\u0103reanu, C.S., Biatek, J., Pressburger, T., Karsai, G., Lowry, M.R., Whalen, M.W.: Integrating statechart components in Polyglot. In: Proc. NASA Formal Methods 2012, pp. 267\u2013272 (2012)"},{"key":"122_CR5","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"298","DOI":"10.1007\/978-3-540-73368-3_34","volume-title":"Proc. 19th Intl. Conf. on Computer Aided Verification (CAV)","author":"C. Barrett","year":"2007","unstructured":"Barrett, C., Tinelli, C.: CVC3. In: Proc. 19th Intl. Conf. on Computer Aided Verification (CAV). LNCS, vol. 4590, pp. 298\u2013302. Springer, Berlin (2007)"},{"key":"122_CR6","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"307","DOI":"10.1007\/978-3-642-00768-2_27","volume-title":"Proc. 15th Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"N. Bj\u00f8rner","year":"2009","unstructured":"Bj\u00f8rner, N., Tillmann, N., Voronkov, A.: Path feasibility analysis for string-manipulating programs. In: Proc. 15th Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 5505, pp. 307\u2013321. Springer, Berlin (2009)"},{"key":"122_CR7","doi-asserted-by":"crossref","first-page":"111","DOI":"10.1109\/ICST.2012.91","volume-title":"Proc. 2012 IEEE Fifth International Conference on Software Testing, Verification and Validation (ICST)","author":"M. Borges","year":"2012","unstructured":"Borges, M., D\u2019Amorim, M., Anand, S., Bushnell, D., P\u0103s\u0103reanu, C.S.: Symbolic execution with interval solving and meta-heuristic search. In: Proc. 2012 IEEE Fifth International Conference on Software Testing, Verification and Validation (ICST), pp. 111\u2013120 (2012)"},{"issue":"7","key":"122_CR8","doi-asserted-by":"crossref","first-page":"775","DOI":"10.1002\/(SICI)1097-024X(200006)30:7<775::AID-SPE309>3.0.CO;2-H","volume":"30","author":"W. Bush","year":"2000","unstructured":"Bush, W., Pincus, J., Sielaff, D.: A static analyzer for finding dynamic programming errors. Softw. Pract. Exp. 30(7), 775\u2013802 (2000)","journal-title":"Softw. Pract. Exp."},{"key":"122_CR9","volume-title":"Numerical Software Verification Workshop, NSV-2011","author":"D. Bushnell","year":"2011","unstructured":"Bushnell, D.: Continuity analysis for floating point software. In: Numerical Software Verification Workshop, NSV-2011 (2011)"},{"key":"122_CR10","first-page":"209","volume-title":"Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation, OSDI\u201908","author":"C. Cadar","year":"2008","unstructured":"Cadar, C., Dunbar, D., Engler, D.: KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In: Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation, OSDI\u201908, pp. 209\u2013224. USENIX Association, Berkeley (2008a)"},{"issue":"2","key":"122_CR11","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1455518.1455522","volume":"12","author":"C. Cadar","year":"2008","unstructured":"Cadar, C., Ganesh, V., Pawlowski, P., Dill, D., Engler, D.: EXE: automatically generating inputs of death. ACM Trans. Inf. Syst. Secur. 12(2), 1\u201338 (2008b)","journal-title":"ACM Trans. Inf. Syst. Secur."},{"key":"122_CR12","doi-asserted-by":"crossref","first-page":"1066","DOI":"10.1145\/1985793.1985995","volume-title":"Proc. 33rd International Conference on Software Engineering (ICSE)","author":"C. Cadar","year":"2011","unstructured":"Cadar, C., Godefroid, P., Khurshid, S., P\u0103s\u0103reanu, C.S., Sen, K., Tillmann, N., Visser, W.: Symbolic execution for software testing in practice: preliminary assessment. In: Proc. 33rd International Conference on Software Engineering (ICSE), pp. 1066\u20131071 (2011)"},{"key":"122_CR13","unstructured":"CERT\/CC: Cert Advisory: multiple vulnerabilities in WU-FTPD. Tech. Rep. CA\u20132001\u201333 (2001)"},{"key":"122_CR14","unstructured":"Choco: Java constraint solver (2012). http:\/\/choco.emn.fr"},{"key":"122_CR15","series-title":"LNCS","first-page":"1","volume-title":"Proc. 10th Intl. Symposium on Static Analysis (SAS)","author":"A.S. Cristensen","year":"2003","unstructured":"Cristensen, A.S., M\u00f8ller, A., Schwartzbach, M.I.: Precise analysis of string expressions. In: Proc. 10th Intl. Symposium on Static Analysis (SAS). LNCS, vol. 2694, pp. 1\u201318. Springer, Berlin (2003)"},{"key":"122_CR16","doi-asserted-by":"crossref","first-page":"215","DOI":"10.1109\/TSE.1976.233817","volume":"2","author":"L.A. Clarke","year":"1976","unstructured":"Clarke, L.A.: A system to generate test data and symbolically execute programs. IEEE Trans. Softw. Eng. 2, 215\u2013222 (1976). doi: 10.1109\/TSE.1976.233817 , http:\/\/dl.acm.org\/citation.cfm?id=1313320.1313532","journal-title":"IEEE Trans. Softw. Eng."},{"key":"122_CR17","first-page":"151","volume-title":"Proc. ESEC\/SIGSOFT FSE","author":"A. Coen-Porisini","year":"2001","unstructured":"Coen-Porisini, A., Denaro, G., Ghezzi, C., Pezz\u00e9, M.: Using symbolic execution for verifying safety-critical systems. In: Proc. ESEC\/SIGSOFT FSE, p. 151. ACM Press, New York (2001)"},{"key":"122_CR18","doi-asserted-by":"crossref","first-page":"315","DOI":"10.1145\/1966445.1966475","volume-title":"Proc. of the 6th Conference on Computer Systems, EuroSys\u201911","author":"P. Collingbourne","year":"2011","unstructured":"Collingbourne, P., Cadar, C., Kelly, P.H.: Symbolic crosschecking of floating-point and simd code. In: Proc. of the 6th Conference on Computer Systems, EuroSys\u201911, pp. 315\u2013328. ACM Press, New York (2011). doi: 10.1145\/1966445.1966475"},{"key":"122_CR19","doi-asserted-by":"crossref","first-page":"59","DOI":"10.1109\/ASE.2006.13","volume-title":"Proc. 21st IEEE\/ACM Intl. Conf. on Automated Software Engineering (ASE)","author":"M. d\u2019Amorim","year":"2006","unstructured":"d\u2019Amorim, M., Pacheco, C., Xie, T., Marinov, D., Ernst, M.D.: An empirical comparison of automated generation and classification techniques for object-oriented unit testing. In: Proc. 21st IEEE\/ACM Intl. Conf. on Automated Software Engineering (ASE), pp. 59\u201368. IEEE Computer Society, Washington (2006)"},{"key":"122_CR20","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Proc. 14th Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Proc. 14th Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 4963, pp. 337\u2013340. Springer, Berlin (2008)"},{"key":"122_CR21","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1109\/ASE.2006.26","volume-title":"Proc. 21st IEEE\/ACM Intl. Conf. on Automated Software Engineering (ASE)","author":"X. Deng","year":"2006","unstructured":"Deng, X., Lee, J., Robby: Bogor\/Kiasan: a k-bounded symbolic execution for checking strong heap properties of open systems. In: Proc. 21st IEEE\/ACM Intl. Conf. on Automated Software Engineering (ASE), pp. 157\u2013166. IEEE Computer Society, Washington (2006)"},{"key":"122_CR22","first-page":"3","volume-title":"3rd International Workshop TAIC PART\u2014Mutation Analysis","author":"X. Deng","year":"2007","unstructured":"Deng, X., Hatcliff, J., Robby: Kiasan\/KUnit: automatic test case generation and analysis feedback for open object-oriented systems. In: 3rd International Workshop TAIC PART\u2014Mutation Analysis, pp. 3\u201312 (2007)"},{"key":"122_CR23","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1007\/s10515-011-0089-9","volume":"19","author":"X. Deng","year":"2012","unstructured":"Deng, X., Lee, J., Robby: Efficient and formal generalized symbolic execution. Autom. Softw. Eng. 19, 233\u2013301 (2012). doi: 10.1007\/s10515-011-0089-9","journal-title":"Autom. Softw. Eng."},{"key":"122_CR24","unstructured":"Detlefs, D.L., Leino, K.R.M., Nelson, G., Saxe, J.B.: Extended static checking. SRC Research Report 159. COMPAQ Systems Research Center (1998)"},{"key":"122_CR25","volume-title":"Proc. 35th International Conference on Software Engineering (ICSE)","author":"A. Filieri","year":"2013","unstructured":"Filieri, A., P\u0103s\u0103reanu, C.S., Visser, W.: Reliability analysis in symbolic PathFinder. In: Proc. 35th International Conference on Software Engineering (ICSE) (2013)"},{"key":"122_CR26","first-page":"166","volume-title":"Proc. International Symposium on Software Testing and Analysis (ISSTA)","author":"J. Geldenhuys","year":"2012","unstructured":"Geldenhuys, J., Dwyer, M.B., Visser, W.: Probabilistic symbolic execution. In: Proc. International Symposium on Software Testing and Analysis (ISSTA), pp. 166\u2013176 (2012)"},{"key":"122_CR27","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1145\/1065010.1065036","volume-title":"Proceedings of the 2005 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)","author":"P. Godefroid","year":"2005","unstructured":"Godefroid, P., Klarlund, N., Sen, K.: Dart: directed automated random testing. In: Proceedings of the 2005 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pp. 213\u2013223. ACM Press, New York (2005)"},{"issue":"5","key":"122_CR28","doi-asserted-by":"crossref","first-page":"30","DOI":"10.1109\/MS.2008.109","volume":"25","author":"P. Godefroid","year":"2008","unstructured":"Godefroid, P., de Halleux, P., Nori, A., Rajamani, S., Schulte, W., Tillmann, N., Levin, M.: Automating software testing using program analysis. IEEE Softw. 25(5), 30\u201337 (2008)","journal-title":"IEEE Softw."},{"key":"122_CR29","doi-asserted-by":"crossref","first-page":"188","DOI":"10.1145\/1542476.1542498","volume-title":"Proc. 2009 ACM SIGPLAN Conf. on Programming Language Design and Implementation (PLDI)","author":"P. Hooimeijer","year":"2009","unstructured":"Hooimeijer, P., Weimer, W.: A decision procedure for subset constraints over regular languages. In: Proc. 2009 ACM SIGPLAN Conf. on Programming Language Design and Implementation (PLDI), pp. 188\u2013198. ACM Press, New York (2009)"},{"key":"122_CR30","doi-asserted-by":"crossref","first-page":"377","DOI":"10.1145\/1858996.1859080","volume-title":"Proc. 25th IEEE\/ACM Intl. Conf. on Automated Software Engineering (ASE)","author":"P. Hooimeijer","year":"2010","unstructured":"Hooimeijer, P., Weimer, W.: Solving string constraints lazily. In: Pecheur, C., Andrews, J. (eds.) Proc. 25th IEEE\/ACM Intl. Conf. on Automated Software Engineering (ASE), pp. 377\u2013386. ACM Press, New York (2010)"},{"key":"122_CR31","unstructured":"Hooimeijer, P., Molnar, D., Saxena, P., Veanes, M.: Modeling imperative string operations with transducers. Tech. Rep. MSR\u2013TR\u20132010\u201396, Microsoft (2010)"},{"key":"122_CR32","unstructured":"IASolver: IASolver page (2010). http:\/\/www.cs.brandeis.edu\/~tim\/Applets\/IAsolver.html"},{"key":"122_CR33","volume-title":"NASA Formal Methods Symposium, NASA Technical Memorandum","author":"K. Jayaraman","year":"2009","unstructured":"Jayaraman, K., Harvison, D., Ganesh, V., Kiezun, A.: JFuzz: a concolic whitebox fuzzer for Java. In: NASA Formal Methods Symposium, NASA Technical Memorandum (2009)"},{"key":"122_CR34","unstructured":"JPF: JPF project (2012). http:\/\/babelfish.arc.nasa.gov\/trac\/jpf"},{"key":"122_CR35","doi-asserted-by":"crossref","first-page":"553","DOI":"10.1007\/3-540-36577-X_40","volume-title":"Proc. 9th Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"S. Khurshid","year":"2003","unstructured":"Khurshid, S., P\u0103s\u0103reanu, C.S., Visser, W.: Generalized symbolic execution for model checking and testing. In: Proc. 9th Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp. 553\u2013568 (2003)"},{"key":"122_CR36","unstructured":"Kie\u017cun, A.: Effective software testing with a string-constraint solver. PhD thesis, Massachusetts Institute of Technology, USA (2009)"},{"key":"122_CR37","first-page":"105","volume-title":"Proc. 2009 International Symposium on Software Testing and Analysis (ISSTA)","author":"A. Kie\u017cun","year":"2009","unstructured":"Kie\u017cun, A., Ganesh, V., Guo, P.J., Hooimeijer, P., Ernst, M.D.: HAMPI: a solver for string constraints. In: Rothermel, G., Dillon, L.K. (eds.) Proc. 2009 International Symposium on Software Testing and Analysis (ISSTA), pp. 105\u2013116. ACM Press, New York (2009)"},{"key":"122_CR38","doi-asserted-by":"crossref","first-page":"385","DOI":"10.1145\/360248.360252","volume":"19","author":"J.C. King","year":"1976","unstructured":"King, J.C.: Symbolic execution and program testing. Commun. ACM 19, 385\u2013394 (1976). doi: 10.1145\/360248.360252","journal-title":"Commun. ACM"},{"key":"122_CR39","unstructured":"LattE: LattE Integrale. UC Davis, Mathematics (2012). http:\/\/www.math.ucdavis.edu\/~latte"},{"key":"122_CR40","doi-asserted-by":"crossref","first-page":"609","DOI":"10.1007\/978-3-642-22110-1_49","volume-title":"Proceedings of the 23rd International Conference on Computer Aided Verification, CAV\u201911","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: Proceedings of the 23rd International Conference on Computer Aided Verification, CAV\u201911, pp. 609\u2013615. Springer, Berlin (2011). http:\/\/dl.acm.org\/citation.cfm?id=2032305.2032354"},{"key":"122_CR41","volume-title":"Asian Symposium on Programming Languages and Systems (APLAS)","author":"X. Li","year":"2008","unstructured":"Li, X., Shannon, D., Ghosh, I., Ogawa, M., Rajan, S., Khurshid, S.: Context-sensitive relevancy analysis for efficient symbolic execution. In: Asian Symposium on Programming Languages and Systems (APLAS) (2008)"},{"key":"122_CR42","unstructured":"Loera, J.A.D., Dutra, B., K\u00f6ppe, M., Moreinis, S., Pinto, G., Wu, J.: Software for exact integration of polynomials over polyhedra (2011). arXiv:1108.0117v2 [math.MG]"},{"key":"122_CR43","volume-title":"JPF Workshop","author":"N. Mirzaei","year":"2012","unstructured":"Mirzaei, N., Malek, S., P\u0103s\u0103reanu, C., Esfahani, N., Mahmood, R.: Testing Android apps through symbolic execution. In: JPF Workshop (2012)"},{"key":"122_CR44","series-title":"LNCS","first-page":"164","volume-title":"Proc. of 11th International SPIN Workshop (SPIN)","author":"C.S. P\u0103s\u0103reanu","year":"2004","unstructured":"P\u0103s\u0103reanu, C.S., Visser, W.: Verification of Java programs using symbolic execution and invariant generation. In: Proc. of 11th International SPIN Workshop (SPIN). LNCS, vol. 2989, pp. 164\u2013181. Springer, Berlin (2004)"},{"key":"122_CR45","doi-asserted-by":"crossref","first-page":"15","DOI":"10.1145\/1390630.1390635","volume-title":"Proc. 2008 International Symposium on Software Testing and Analysis (ISSTA)","author":"C.S. P\u0103s\u0103reanu","year":"2008","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: Proc. 2008 International Symposium on Software Testing and Analysis (ISSTA), pp. 15\u201326 (2008)"},{"key":"122_CR46","doi-asserted-by":"crossref","first-page":"34","DOI":"10.1145\/2001420.2001425","volume-title":"Proceedings of the 2011 International Symposium on Software Testing and Analysis (ISSTA)","author":"C.S. P\u0103s\u0103reanu","year":"2011","unstructured":"P\u0103s\u0103reanu, C.S., Rungta, N., Visser, W.: Symbolic execution with mixed concrete-symbolic solving. In: Proceedings of the 2011 International Symposium on Software Testing and Analysis (ISSTA), pp. 34\u201344. ACM Press, New York (2011). doi: 10.1145\/2001420.2001425"},{"key":"122_CR47","first-page":"504","volume-title":"Proc. 2011 ACM SIGPLAN Conf. on Programming Language Design and Implementation (PLDI)","author":"S. Person","year":"2011","unstructured":"Person, S., Yang, G., Rungta, N., Khurshid, S.: Directed incremental symbolic execution. In: Proc. 2011 ACM SIGPLAN Conf. on Programming Language Design and Implementation (PLDI), pp. 504\u2013515 (2011)"},{"key":"122_CR48","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/2382756.2382791","volume":"37","author":"Q.-S. Phan","year":"2012","unstructured":"Phan, Q.-S., Malacaria, P., Tkachuk, O., P\u0103s\u0103reanu, C.S.: Symbolic quantitative information flow. Softw. Eng. Notes 37, 1\u20135 (2012)","journal-title":"Softw. Eng. Notes"},{"key":"122_CR49","volume-title":"Proc. 31st International Conference on Software Engineering (ICSE Companion)","author":"S. Rajan","year":"2009","unstructured":"Rajan, S., Tkachuk, O., Prasad, M., Ghosh, I., Goel, N., Uehara, T.: WEAVE: WEb Applications Validation Environment. In: Proc. 31st International Conference on Software Engineering (ICSE Companion) (2009)"},{"key":"122_CR50","unstructured":"Redelinghuys, G.: Symbolic string execution. Master\u2019s thesis, Stellenbosch University (2012)"},{"key":"122_CR51","unstructured":"Redis: Redis NoSQL database (2012). http:\/\/redis.io"},{"key":"122_CR52","volume-title":"Handbook of Constraint Programming","author":"F. Rossi","year":"2006","unstructured":"Rossi, F., van Beek, P., Walsh, T.: Handbook of Constraint Programming. Elsevier, Amsterdam (2006)"},{"key":"122_CR53","first-page":"174","volume-title":"Proc. of 16th International SPIN Workshop (SPIN)","author":"N. Rungta","year":"2009","unstructured":"Rungta, N., Mercer, E.G., Visser, W.: Efficient testing of concurrent programs with abstraction-guided symbolic execution. In: Proc. of 16th International SPIN Workshop (SPIN), pp. 174\u2013191 (2009)"},{"key":"122_CR54","volume-title":"Redis: the Definitive Guide","author":"S. Sanfilippo","year":"2012","unstructured":"Sanfilippo, S., Noordhuis, P.: Redis: the Definitive Guide. O\u2019Reilly Media, Sebastopol (2012)"},{"key":"122_CR55","first-page":"195","volume-title":"Proc. 2010 International Symposium on Software Testing and Analysis (ISSTA)","author":"R. Santelices","year":"2010","unstructured":"Santelices, R., Harrold, M.J.: Exploiting program dependencies for scalable multiple-path symbolic execution. In: Proc. 2010 International Symposium on Software Testing and Analysis (ISSTA), pp. 195\u2013206 (2010)"},{"key":"122_CR56","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1109\/ICDCS.2011.28","volume-title":"Proceedings of the 2011 31st International Conference on Distributed Computing Systems, ICDCS \u201911","author":"R. Sasnauskas","year":"2011","unstructured":"Sasnauskas, R., Dustmann, O.S., Kaminski, B.L., Wehrle, K., Weise, C., Kowalewski, S.: Scalable symbolic execution of distributed systems. In: Proceedings of the 2011 31st International Conference on Distributed Computing Systems, ICDCS \u201911, pp. 333\u2013342. IEEE Computer Society, Washington (2011). doi: 10.1109\/ICDCS.2011.28"},{"key":"122_CR57","first-page":"513","volume-title":"Proc. 31st IEEE Symposium on Security and Privacy","author":"P. Saxena","year":"2010","unstructured":"Saxena, P., Akhawe, D., Hanna, S., Mao, F., McCamant, S., Song, D.: A symbolic execution framework for JavaScript. In: Proc. 31st IEEE Symposium on Security and Privacy, pp. 513\u2013528. IEEE Computer Society, Washington (2010)"},{"key":"122_CR58","doi-asserted-by":"crossref","first-page":"419","DOI":"10.1007\/11817963_38","volume-title":"Proc. 18th International Conference on Computer Aided Verification (CAV)","author":"K. Sen","year":"2006","unstructured":"Sen, K., Agha, G.: CUTE and jCUTE: concolic unit testing and explicit path model-checking tools. In: Proc. 18th International Conference on Computer Aided Verification (CAV), pp. 419\u2013423 (2006)"},{"key":"122_CR59","series-title":"LNCS","first-page":"166","volume-title":"Proc. Haifa Verification Conference (HVC)","author":"K. Sen","year":"2007","unstructured":"Sen, K., Agha, G.: A race-detection and flipping algorithm for automated testing of multithreaded programs. In: Proc. Haifa Verification Conference (HVC). LNCS, vol. 4383, pp. 166\u2013182. Springer, Berlin (2007)"},{"key":"122_CR60","first-page":"13","volume-title":"Proc. Testing: Academic and Industrial Conf. Practice and Research Techniques","author":"D. Shannon","year":"2007","unstructured":"Shannon, D., Hajra, S., Lee, A., Zhan, D., Khurshid, S.: Abstracting symbolic execution with string analysis. In: Proc. Testing: Academic and Industrial Conf. Practice and Research Techniques, pp. 13\u201322. IEEE Computer Society, Washington (2007)"},{"key":"122_CR61","first-page":"22","volume-title":"Proc. 2nd Intl. Workshop on Defects in Large Software Systems","author":"D. Shannon","year":"2009","unstructured":"Shannon, D., Ghosh, I., Rajan, S.P., Khurshid, S.: Efficient symbolic execution of strings for validating web applications. In: Proc. 2nd Intl. Workshop on Defects in Large Software Systems, pp. 22\u201326. ACM Press, New York (2009)"},{"key":"122_CR62","doi-asserted-by":"crossref","first-page":"395","DOI":"10.1007\/s11786-011-0100-7","volume":"5","author":"S. Siegel","year":"2011","unstructured":"Siegel, S., Zirkel, T.: Tass: the toolkit for accurate scientific software. Math. Comput. Sci. 5, 395\u2013426 (2011). doi: 10.1007\/s11786-011-0100-7","journal-title":"Math. Comput. Sci."},{"key":"122_CR63","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1145\/1146238.1146256","volume-title":"Proc. 2006 International Symposium on Software Testing and Analysis (ISSTA)","author":"S. Siegel","year":"2006","unstructured":"Siegel, S., Mironova, A., Avrunin, G., Clarke, L.: Using model checking with symbolic execution to verify parallel numerical programs. In: Proc. 2006 International Symposium on Software Testing and Analysis (ISSTA), pp. 157\u2013168. ACM Press, New York (2006)"},{"key":"122_CR64","doi-asserted-by":"crossref","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: NASA Formal Methods, pp. 359\u2013374 (2011)"},{"key":"122_CR65","unstructured":"SPF: Symbolic Pathfinder (jpf-symbc) (2012). http:\/\/babelfish.arc.nasa.gov\/trac\/jpf"},{"key":"122_CR66","first-page":"183","volume-title":"Proc. 2010 International Symposium on Software Testing and Analysis (ISSTA)","author":"M. Staats","year":"2010","unstructured":"Staats, M., P\u0103s\u0103reanu, C.: Parallel symbolic execution for structural test generation. In: Proc. 2010 International Symposium on Software Testing and Analysis (ISSTA), pp. 183\u2013194. ACM Press, New York (2010). doi: 10.1007\/s10515-013-0122-2"},{"key":"122_CR67","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/978-3-540-79124-9_10","volume-title":"Proc. 2nd Intl. Conf. on 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.) Proc. 2nd Intl. Conf. on Tests and Proofs. LNCS, vol. 4966, pp. 134\u2013153. Springer, Berlin (2008)"},{"key":"122_CR68","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1145\/1273463.1273478","volume-title":"Proc. 2007 International Symposium on Software Testing and Analysis (ISSTA)","author":"A. Tomb","year":"2007","unstructured":"Tomb, A., Brat, G., Visser, W.: Variably interprocedural program analysis for run-time error detection. In: Proc. 2007 International Symposium on Software Testing and Analysis (ISSTA), pp. 97\u2013107. ACM Press, New York (2007)"},{"key":"122_CR69","first-page":"498","volume-title":"Proc. 3rd Intl. Conf. on Software Testing, Verification and Validation","author":"M. Veanes","year":"2010","unstructured":"Veanes, M., de Halleux, P., Tillmann, N.: Rex: symbolic regular expression explorer. In: Proc. 3rd Intl. Conf. on Software Testing, Verification and Validation, pp. 498\u2013507. IEEE Computer Society, Washington (2010)"},{"issue":"2","key":"122_CR70","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1023\/A:1022920129859","volume":"10","author":"W. Visser","year":"2003","unstructured":"Visser, W., Havelund, K., Brat, G.P., Park, S., Lerda, F.: Model checking programs. Autom. Softw. Eng. 10(2), 203\u2013232 (2003)","journal-title":"Autom. Softw. Eng."},{"key":"122_CR71","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1145\/1146238.1146243","volume-title":"Proc. 2006 International Symposium on Software Testing and Analysis (ISSTA)","author":"W. Visser","year":"2006","unstructured":"Visser, W., P\u0103s\u0103reanu, C.S., Pel\u00e1nek, R.: Test input generation for Java containers using state matching. In: Proc. 2006 International Symposium on Software Testing and Analysis (ISSTA), pp. 37\u201348 (2006)"},{"key":"122_CR72","volume-title":"International Symposium on the Foundations of Software Engineering (FSE)","author":"W. Visser","year":"2012","unstructured":"Visser, W., Geldenhuys, J., Dwyer, M.B.: Green: reducing, reusing and recycling constraints in program analysis. In: International Symposium on the Foundations of Software Engineering (FSE), Cary, North Carolina, USA (2012)"},{"key":"122_CR73","doi-asserted-by":"crossref","first-page":"365","DOI":"10.1007\/978-3-540-31980-1_24","volume-title":"Proceedings of the 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"T. Xie","year":"2005","unstructured":"Xie, T., Marinov, D., Schulte, W., Notkin, D.: Symstra: a framework for generating object-oriented unit tests using symbolic execution. In: Proceedings of the 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp. 365\u2013381. Springer, Berlin (2005)"},{"key":"122_CR74","first-page":"144","volume-title":"Proc. International Symposium on Software Testing and Analysis (ISSTA)","author":"G. Yang","year":"2012","unstructured":"Yang, G., P\u0103s\u0103reanu, C.S., Khurshid, S.: Memoized symbolic execution. In: Proc. International Symposium on Software Testing and Analysis (ISSTA), pp. 144\u2013154 (2012)"},{"key":"122_CR75","unstructured":"Yices: Yices SMT Solver (2012). http:\/\/yices.csl.sri.com\/"},{"key":"122_CR76","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"306","DOI":"10.1007\/978-3-540-85114-1_21","volume-title":"Proc. 15th Intl. SPIN Workshop on Model Checking Software","author":"F. Yu","year":"2008","unstructured":"Yu, F., Bultan, T., Cova, M., Ibarra, O.H.: Symbolic string verification: an automata-based approach. In: Proc. 15th Intl. SPIN Workshop on Model Checking Software. LNCS, vol. 5156, pp. 306\u2013324. Springer, Berlin (2008)"},{"key":"122_CR77","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"154","DOI":"10.1007\/978-3-642-12002-2_13","volume-title":"Proc. 16th Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"F. Yu","year":"2010","unstructured":"Yu, F., Alkhalaf, M., Bultan, T.: Stranger: an automata-based string analysis tool for PHP. In: Proc. 16th Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 6015, pp. 154\u2013157. Springer, Berlin (2010)"},{"key":"122_CR78","first-page":"43","volume-title":"Proc. 26th IEEE\/ACM Intl. Conf. on Automated Software Engineering","author":"P. Zhang","year":"2011","unstructured":"Zhang, P., Elbaum, S.G., Dwyer, M.B.: Automatic generation of load tests. In: Alexander, P., P\u0103s\u0103reanu, C.S., Hosking, J.G. (eds.) Proc. 26th IEEE\/ACM Intl. Conf. on Automated Software Engineering, pp. 43\u201352. IEEE Press, New York (2011)"}],"container-title":["Automated Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10515-013-0122-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10515-013-0122-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10515-013-0122-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,2,9]],"date-time":"2022-02-09T12:02:31Z","timestamp":1644408151000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10515-013-0122-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,2,26]]},"references-count":78,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2013,9]]}},"alternative-id":["122"],"URL":"https:\/\/doi.org\/10.1007\/s10515-013-0122-2","relation":{},"ISSN":["0928-8910","1573-7535"],"issn-type":[{"value":"0928-8910","type":"print"},{"value":"1573-7535","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,2,26]]}}}