{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:21:51Z","timestamp":1751660511064,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662468227"},{"type":"electronic","value":"9783662468234"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-46823-4_27","type":"book-chapter","created":{"date-parts":[[2015,4,18]],"date-time":"2015-04-18T01:40:54Z","timestamp":1429321254000},"page":"335-350","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Symbolic String Transformations with Regular Lookahead and Rollback"],"prefix":"10.1007","author":[{"given":"Margus","family":"Veanes","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,4,19]]},"reference":[{"key":"27_CR1","doi-asserted-by":"crossref","unstructured":"Alur, R., Cern\u00fd, P.: Streaming transducers for algorithmic verification of single-pass list-processing programs. In: POPL 2011, pp. 599\u2013610. ACM (2011)","DOI":"10.1145\/1925844.1926454"},{"key":"27_CR2","doi-asserted-by":"crossref","unstructured":"Alur, R., Filiot, E., Trivedi, A.: Regular transformations of infinite strings. In: LICS, pp. 65\u201374. IEEE (2012)","DOI":"10.1109\/LICS.2012.18"},{"key":"27_CR3","doi-asserted-by":"crossref","unstructured":"Balzarotti, D., Cova, M., Felmetsger, V., Jovanovic, N., Kirda, E., Kruegel, C., Vigna, G.: Saner: composing static and dynamic analysis to validate sanitization in web applications. In: SP 2008, pp. 387\u2013401. IEEE (2008)","DOI":"10.1109\/SP.2008.22"},{"key":"27_CR4","unstructured":"Bex (2013). http:\/\/www.rise4fun.com\/Bex\/tutorial"},{"key":"27_CR5","doi-asserted-by":"crossref","unstructured":"Botincan, M., Babic, D.: Sigma*: symbolic learning of input-output specifications. In: POPL 2013, pp. 443\u2013456. ACM (2013)","DOI":"10.1145\/2480359.2429123"},{"key":"27_CR6","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":"AS Christensen","year":"2003","unstructured":"Christensen, A.S., M\u00f8ller, A., Schwartzbach, M.I.: Precise analysis of string. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 1\u201318. Springer, Heidelberg (2003)"},{"key":"27_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"624","DOI":"10.1007\/978-3-642-39799-8_41","volume-title":"Computer Aided Verification","author":"L D\u2019Antoni","year":"2013","unstructured":"D\u2019Antoni, L., Veanes, M.: Equivalence of extended symbolic finite transducers. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 624\u2013639. Springer, Heidelberg (2013)"},{"key":"27_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/978-3-642-35873-9_14","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"L D\u2019Antoni","year":"2013","unstructured":"D\u2019Antoni, L., Veanes, M.: Static analysis of string encoders and decoders. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 209\u2013228. Springer, Heidelberg (2013)"},{"key":"27_CR9","doi-asserted-by":"crossref","unstructured":"Dantoni, L., Veanes, M.: Minimization of symbolic automata. In: POPL 2014. ACM (2014)","DOI":"10.1145\/2535838.2535849"},{"key":"27_CR10","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 de Moura","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. 4963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"27_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/978-3-540-74061-2_4","volume-title":"Static Analysis","author":"T Le Gall","year":"2007","unstructured":"Le Gall, T., Jeannet, B.: Lattice automata: a representation for languages on infinite alphabets, and some applications to verification. In: Riis Nielson, H., Fil\u00e9, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 52\u201368. Springer, Heidelberg (2007)"},{"key":"27_CR12","doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Compositional dynamic test generation. In: POPL 2007, pp. 47\u201354(2007)","DOI":"10.1145\/1190215.1190226"},{"key":"27_CR13","unstructured":"Hooimeijer, P., Livshits, B., Molnar, D., Saxena, P., Veanes, M.: Fast and precise sanitizer analysis with Bek. In: USENIX Security, August 2011"},{"issue":"2","key":"27_CR14","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1016\/0304-3975(94)90242-9","volume":"134","author":"M Kaminski","year":"1994","unstructured":"Kaminski, M., Francez, N.: Finite-memory automata. TCS 134(2), 329\u2013363 (1994)","journal-title":"TCS"},{"key":"27_CR15","doi-asserted-by":"crossref","unstructured":"Kumar, S., Chandrasekaran, B., Turner, J., Varghese, G.: Curing regular expressions matching algorithms from insomnia, amnesia, and acalculia. In: ANCS 2007, pp. 155\u2013164. ACM\/IEEE (2007)","DOI":"10.1145\/1323548.1323574"},{"key":"27_CR16","doi-asserted-by":"crossref","unstructured":"Livshits, B., Nori, A.V., Rajamani, S.K., Banerjee, A.: Merlin: specification inference for explicit information flow problems. In: PLDI 2009, pp. 75\u201386 (2009)","DOI":"10.1145\/1543135.1542485"},{"key":"27_CR17","doi-asserted-by":"crossref","unstructured":"Minamide, Y.: Static approximation of dynamically generated web pages. In: WWW 2005, pp. 432\u2013441 (2005)","DOI":"10.1145\/1060745.1060809"},{"key":"27_CR18","unstructured":"NVD. http:\/\/web.nvd.nist.gov\/view\/vuln\/detail?vulnId=CVE-2008-2938"},{"key":"27_CR19","unstructured":"OWASP. https:\/\/www.owasp.org\/index.php\/Double_Encoding"},{"key":"27_CR20","unstructured":"SANS. http:\/\/www.sans.org\/security-resources\/malwarefaq\/wnt-unicode.php"},{"key":"27_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/11874683_3","volume-title":"Computer Science Logic","author":"L Segoufin","year":"2006","unstructured":"Segoufin, L.: Automata and logics for words and trees over an infinite alphabet. In: \u00c9sik, Z. (ed.) CSL 2006. LNCS, vol. 4207, pp. 41\u201357. Springer, Heidelberg (2006)"},{"key":"27_CR22","doi-asserted-by":"crossref","unstructured":"Smith, R., Estan, C., Jha, S., Kong, S.: Deflating the big bang: fast and scalable deep packet inspection with extended finite automata. In: SIGCOMM 2008, pp. 207\u2013218. ACM (2008)","DOI":"10.1145\/1402958.1402983"},{"key":"27_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1007\/978-3-642-29709-0_32","volume-title":"Perspectives of Systems Informatics","author":"M Veanes","year":"2012","unstructured":"Veanes, M., Bj\u00f8rner, N.: Symbolic tree transducers. In: Clarke, E., Virbitskaite, I., Voronkov, A. (eds.) PSI 2011. LNCS, vol. 7162, pp. 377\u2013393. Springer, Heidelberg (2012)"},{"key":"27_CR24","doi-asserted-by":"crossref","unstructured":"Veanes, M., Hooimeijer, P., Livshits, B., Molnar, D., Bj\u00f8rner, N.: Symbolic finite state transducers: algorithms and applications. In: POPL 2012, pp. 137\u2013150 (2012)","DOI":"10.1145\/2103621.2103674"},{"key":"27_CR25","doi-asserted-by":"crossref","unstructured":"Wassermann, G., Yu, D., Chander, A., Dhurjati, D., Inamura, H., Su, Z.: Dynamic test input generation for web applications. In: ISSTA (2008)","DOI":"10.1145\/1390630.1390661"},{"key":"27_CR26","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-3-642-59136-5_2","volume-title":"Handbook of Formal Languages","author":"S Yu","year":"1997","unstructured":"Yu, S.: Regular languages. In: Rozenberg, G., Salomaa, A. (eds.) Handbook of Formal Languages, vol. 1, pp. 41\u2013110. Springer, Heidelberg (1997)"},{"key":"27_CR27","unstructured":"Z3. http:\/\/research.microsoft.com\/projects\/z3"}],"container-title":["Lecture Notes in Computer Science","Perspectives of System Informatics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-46823-4_27","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,21]],"date-time":"2023-02-21T00:40:54Z","timestamp":1676940054000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-662-46823-4_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662468227","9783662468234"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-46823-4_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"19 April 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}