{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,25]],"date-time":"2026-10-25T15:33:06Z","timestamp":1792942386129,"version":"4.5.0"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642007675","type":"print"},{"value":"9783642007682","type":"electronic"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-00768-2_27","type":"book-chapter","created":{"date-parts":[[2009,3,27]],"date-time":"2009-03-27T01:16:10Z","timestamp":1238116570000},"page":"307-321","source":"Crossref","is-referenced-by-count":109,"title":["Path Feasibility Analysis for String-Manipulating Programs"],"prefix":"10.1007","author":[{"given":"Nikolaj","family":"Bj\u00f8rner","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Nikolai","family":"Tillmann","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Andrei","family":"Voronkov","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"27_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/11609773_28","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A.R. Bradley","year":"2005","unstructured":"Bradley, A.R., Manna, Z., Sipma, H.B.: What\u2019s decidable about arrays? In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol.\u00a03855, pp. 427\u2013442. Springer, Heidelberg (2005)"},{"key":"27_CR2","doi-asserted-by":"crossref","unstructured":"B\u00fcchi, J.R., Senger, S.: Definability in the existential theory of concatenation. Zeitschrift fur Mathematische Logik und Grundlagen der Mathematik (1988)","DOI":"10.1007\/BF02017493"},{"key":"27_CR3","doi-asserted-by":"crossref","first-page":"322","DOI":"10.1145\/1180405.1180445","volume-title":"CCS","author":"C. Cadar","year":"2006","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 Press, New York (2006)"},{"key":"27_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-44898-5_1","volume-title":"Static Analysis","author":"A.S. Christensen","year":"2003","unstructured":"Christensen, A.S., M\u00f8ller, A., Schwartzbach, M.I.: Precise analysis of string expressions. In: Cousot, R. (ed.) SAS 2003. LNCS, vol.\u00a02694, pp. 1\u201318. Springer, Heidelberg (2003)"},{"key":"27_CR5","first-page":"138","volume-title":"VTC Spring","author":"Y. Dong","year":"2008","unstructured":"Dong, Y., Quan, Q., Zhang, J.: Priority-based energy aware and coverage preserving routing for wireless sensor network. In: VTC Spring, pp. 138\u2013142. IEEE, Los Alamitos (2008)"},{"key":"27_CR6","doi-asserted-by":"crossref","unstructured":"Fu, X., Lu, X., Peltsverger, B., Chen, S., Qian, K., Tao, L.: A Static Analysis Framework For Detecting SQL Injection Vulnerabilities. In: COMPSAC, pp. 87\u201396 (2007)","DOI":"10.1109\/COMPSAC.2007.43"},{"key":"27_CR7","first-page":"47","volume-title":"Proc. of POPL 2007","author":"P. Godefroid","year":"2007","unstructured":"Godefroid, P.: Compositional dynamic test generation. In: Proc. of POPL 2007, pp. 47\u201354. ACM Press, New York (2007)"},{"issue":"6","key":"27_CR8","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1145\/1064978.1065036","volume":"40","author":"P. Godefroid","year":"2005","unstructured":"Godefroid, P., Klarlund, N., Sen, K.: DART: directed automated random testing. SIGPLAN Notices\u00a040(6), 213\u2013223 (2005)","journal-title":"SIGPLAN Notices"},{"key":"27_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"474","DOI":"10.1007\/978-3-540-78499-9_33","volume-title":"Foundations of Software Science and Computational Structures","author":"P. Habermehl","year":"2008","unstructured":"Habermehl, P., Iosif, R., Vojnar, T.: What else is decidable about integer arrays? In: Amadio, R. (ed.) FOSSACS 2008. LNCS, vol.\u00a04962, pp. 474\u2013489. Springer, Heidelberg (2008)"},{"key":"27_CR10","doi-asserted-by":"crossref","unstructured":"Khoussainov, B., Nies, A., Rubin, S., Stephan, F.: Automatic structures: Richness and limitations. In: LICS, pp. 44\u201353 (2004)","DOI":"10.1109\/LICS.2004.1319599"},{"issue":"7","key":"27_CR11","doi-asserted-by":"publisher","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\u00a019(7), 385\u2013394 (1976)","journal-title":"Commun. ACM"},{"key":"27_CR12","unstructured":"Matiyasevich, Y.: Word Equations, Fibonacci Numbers, and Hilbert\u2019s Tenth problem. In: Workshop on Fibonacci Words, vol.\u00a043, pp. 36\u201339 (2007)"},{"key":"27_CR13","first-page":"219","volume":"0","author":"H. Ruan","year":"2008","unstructured":"Ruan, H., Zhang, J., Yan, J.: Test Data Generation for C Programs with String-Handling Functions. Theoretical Aspects of Software Engineering\u00a00, 219\u2013226 (2008)","journal-title":"Theoretical Aspects of Software Engineering"},{"key":"27_CR14","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.A.: 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":"27_CR15","doi-asserted-by":"crossref","unstructured":"Shannon, D., Hajra, S., Lee, A., Zhan, D., Khurshid, S.: Abstracting symbolic execution with string analysis. In: Taicpart-Mutation, Washington, DC, USA, pp. 13\u201322 (2007)","DOI":"10.1109\/TAIC.PART.2007.34"},{"key":"27_CR16","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 - white box test generation for .NET. In: Beckert, B., H\u00e4hnle, R. (eds.) TAP 2008. LNCS, vol.\u00a04966, pp. 134\u2013153. Springer, Heidelberg (2008)"},{"key":"27_CR17","doi-asserted-by":"crossref","unstructured":"Xie, T., Tillmann, N., de Halleux, P., Schulte, W.: Fitness-guided path exploration in dynamic symbolic execution. Technical Report MSR-TR-2008-123, Microsoft (2008)","DOI":"10.1109\/DSN.2009.5270315"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-00768-2_27","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,12]],"date-time":"2024-03-12T04:14:59Z","timestamp":1710216899000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-00768-2_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642007675","9783642007682"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-00768-2_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009]]}}}