{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,14]],"date-time":"2026-02-14T00:56:34Z","timestamp":1771030594925,"version":"3.50.1"},"reference-count":44,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2013,9,5]],"date-time":"2013-09-05T00:00:00Z","timestamp":1378339200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2014,2]]},"DOI":"10.1007\/s10703-013-0189-1","type":"journal-article","created":{"date-parts":[[2013,9,4]],"date-time":"2013-09-04T07:27:40Z","timestamp":1378279660000},"page":"44-70","source":"Crossref","is-referenced-by-count":58,"title":["Automata-based symbolic string analysis for vulnerability detection"],"prefix":"10.1007","volume":"44","author":[{"given":"Fang","family":"Yu","sequence":"first","affiliation":[]},{"given":"Muath","family":"Alkhalaf","sequence":"additional","affiliation":[]},{"given":"Tevfik","family":"Bultan","sequence":"additional","affiliation":[]},{"given":"Oscar H.","family":"Ibarra","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2013,9,5]]},"reference":[{"key":"189_CR1","first-page":"947","volume-title":"ICSE","author":"M Alkhalaf","year":"2012","unstructured":"Alkhalaf M, Bultan T, Gallegos JL (2012) Verifying client-side input validation functions using string analysis. In: ICSE, pp 947\u2013957"},{"key":"189_CR2","first-page":"387","volume-title":"S&P","author":"D Balzarotti","year":"2008","unstructured":"Balzarotti D, Cova M, Felmetsger V, Jovanovic N, Kruegel C, Kirda E, Vigna G (2008) Saner: composing static and dynamic analysis to validate sanitization in web applications. In: S&P, pp 387\u2013401"},{"issue":"4","key":"189_CR3","doi-asserted-by":"crossref","first-page":"605","DOI":"10.1142\/S0129054103001911","volume":"14","author":"C Bartzis","year":"2003","unstructured":"Bartzis C, Bultan T (2003) Efficient symbolic representations for arithmetic constraints in verification. Int J Found Comput Sci 14(4):605\u2013624","journal-title":"Int J Found Comput Sci"},{"key":"189_CR4","first-page":"321","volume-title":"CAV","author":"C Bartzis","year":"2004","unstructured":"Bartzis C, Bultan T (2004) Widening arithmetic automata. In: CAV, pp 321\u2013333"},{"key":"189_CR5","first-page":"6","volume-title":"WIA","author":"M Biehl","year":"1997","unstructured":"Biehl M, Klarlund N, Rauhe T (1997) Algorithms for guided tree automata. In: WIA, pp 6\u201325"},{"key":"189_CR6","first-page":"307","volume-title":"TACAS","author":"N Bj\u00f8rner","year":"2009","unstructured":"Bj\u00f8rner N, Tillmann N, Voronkov A (2009) Path feasibility analysis for string-manipulating programs. In: TACAS, pp 307\u2013321"},{"issue":"2","key":"189_CR7","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1109\/T-C.1971.223204","volume":"C-20","author":"R Book","year":"1971","unstructured":"Book R, Even S, Greibach S, Ott G (1971) Ambiguity in graphs and expressions. IEEE Trans Comput C-20(2):149\u2013153","journal-title":"IEEE Trans Comput"},{"key":"189_CR8","first-page":"372","volume-title":"CAV","author":"A Bouajjani","year":"2004","unstructured":"Bouajjani A, Habermehl P, Vojnar T (2004) Abstract regular model checking. In: CAV, pp 372\u2013386"},{"key":"189_CR9","first-page":"403","volume-title":"CAV","author":"A Bouajjani","year":"2000","unstructured":"Bouajjani A, Jonsson B, Nilsson M, Touili T (2000) Regular model checking. In: CAV, pp 403\u2013418"},{"key":"189_CR10","unstructured":"BRICS. The MONA project. http:\/\/www.brics.dk\/mona\/"},{"key":"189_CR11","first-page":"374","volume-title":"APLAS","author":"T-H Choi","year":"2006","unstructured":"Choi T-H, Lee O, Kim H, Doh K-G (2006) A practical string analyzer by the widening approach. In: APLAS, pp 374\u2013388"},{"key":"189_CR12","first-page":"1","volume-title":"SAS","author":"AS Christensen","year":"2003","unstructured":"Christensen AS, M\u00f8ller A, Schwartzbach MI (2003) Precise analysis of string expressions. In: SAS, pp 1\u201318"},{"key":"189_CR13","doi-asserted-by":"crossref","first-page":"88","DOI":"10.1145\/1108792.1108814","volume-title":"PASTE","author":"M Christodorescu","year":"2005","unstructured":"Christodorescu M, Kidd N, Goh W-H (2005) String analysis for x86 binaries. In: PASTE, pp 88\u201395"},{"key":"189_CR14","first-page":"87","volume-title":"COMPSAC","author":"X Fu","year":"2007","unstructured":"Fu X, Lu X, Peltsverger B, Chen S, Qian K, Tao L (2007) A static analysis framework for detecting SQL injection vulnerabilities. In: COMPSAC, pp 87\u201396"},{"key":"189_CR15","first-page":"645","volume-title":"ICSE","author":"C Gould","year":"2004","unstructured":"Gould C, Su Z, Devanbu P (2004) Static checking of dynamically generated queries in database applications. In: ICSE, pp 645\u2013654"},{"key":"189_CR16","first-page":"1","volume-title":"SEC","author":"P Hooimeijer","year":"2011","unstructured":"Hooimeijer P, Livshits B, Molnar D, Saxena P, Veanes M (2011) Fast and precise sanitizer analysis with BEK. In: SEC, p 1"},{"key":"189_CR17","doi-asserted-by":"crossref","first-page":"188","DOI":"10.1145\/1542476.1542498","volume-title":"PLDI","author":"P Hooimeijer","year":"2009","unstructured":"Hooimeijer P, Weimer W (2009) A decision procedure for subset constraints over regular languages. In: PLDI, pp 188\u2013198"},{"issue":"4","key":"189_CR18","doi-asserted-by":"crossref","first-page":"531","DOI":"10.1007\/s10515-012-0111-x","volume":"19","author":"P Hooimeijer","year":"2012","unstructured":"Hooimeijer P, Weimer W (2012) Strsolve: solving string constraints lazily. Autom Softw Eng 19(4):531\u2013559","journal-title":"Autom Softw Eng"},{"key":"189_CR19","first-page":"258","volume-title":"S&P","author":"N Jovanovic","year":"2006","unstructured":"Jovanovic N, Kr\u00fcgel C, Kirda E (2006) Pixy: a static analysis tool for detecting web application vulnerabilities (short paper). In: S&P, pp 258\u2013263"},{"key":"189_CR20","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1145\/1572272.1572286","volume-title":"ISSTA","author":"A Kiezun","year":"2009","unstructured":"Kiezun A, Ganesh V, Guo PJ, Hooimeijer P, Ernst MD (2009) Hampi: a solver for string constraints. In: ISSTA, pp 105\u2013116"},{"issue":"3","key":"189_CR21","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1109\/TSE.2004.1271173","volume":"30","author":"C Kirkegaard","year":"2004","unstructured":"Kirkegaard C, M\u00f8ller A, Schwartzbach MI (2004) Static analysis of XML transformations in Java. IEEE Trans Softw Eng 30(3):181\u2013192","journal-title":"IEEE Trans Softw Eng"},{"issue":"4","key":"189_CR22","doi-asserted-by":"crossref","first-page":"571","DOI":"10.1142\/S012905410200128X","volume":"13","author":"N Klarlund","year":"2002","unstructured":"Klarlund N, M\u00f8ller A, Schwartzbach MI (2002) MONA implementation secrets. Int J Found Comput Sci 13(4):571\u2013586","journal-title":"Int J Found Comput Sci"},{"key":"189_CR23","first-page":"432","volume-title":"WWW","author":"Y Minamide","year":"2005","unstructured":"Minamide Y (2005) Static approximation of dynamically generated web pages. In: WWW, pp 432\u2013441"},{"key":"189_CR24","unstructured":"OWASP. Top 10 2007. https:\/\/www.owasp.org\/index.php\/Top_10_2007"},{"key":"189_CR25","doi-asserted-by":"crossref","unstructured":"OWASP. Top 10 2010. https:\/\/www.owasp.org\/index.php\/Top_10_2010-Main","DOI":"10.1007\/BF03358591"},{"key":"189_CR26","unstructured":"OWASP. Top 10 2013. https:\/\/www.owasp.org\/index.php\/Top_10_2013-T10"},{"issue":"1","key":"189_CR27","first-page":"32","volume":"10","author":"Y Sakuma","year":"2012","unstructured":"Sakuma Y, Minamide Y, Voronkov A (2012) Translating regular expression matching into transducers. J\u00a0Appl Log 10(1):32\u201351","journal-title":"J\u00a0Appl Log"},{"key":"189_CR28","first-page":"513","volume-title":"S&P","author":"P Saxena","year":"2010","unstructured":"Saxena P, Akhawe D, Hanna S, Mao F, McCamant S, Song D (2010) A symbolic execution framework for JavaScript. In: S&P, pp 513\u2013528"},{"key":"189_CR29","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1145\/1081706.1081750","volume-title":"ESEC\/FSE","author":"K Sen","year":"2005","unstructured":"Sen K, Marinov D, Agha G (2005) Cute: a concolic unit testing engine for C. In: ESEC\/FSE, pp 263\u2013272"},{"key":"189_CR30","first-page":"13","volume-title":"TAICPART-MUTATION","author":"D Shannon","year":"2007","unstructured":"Shannon D, Hajra S, Lee A, Zhan D, Khurshid S (2007) Abstracting symbolic execution with string analysis. In: TAICPART-MUTATION, pp 13\u201322"},{"key":"189_CR31","unstructured":"Sourceforge. Open sources. http:\/\/sourceforge.net"},{"key":"189_CR32","first-page":"166","volume-title":"ISSTA","author":"T Tateishi","year":"2011","unstructured":"Tateishi T, Pistoia M, Tripp O (2011) Path- and index-sensitive string analysis based on monadic second-order logic. In: ISSTA, pp 166\u2013176"},{"key":"189_CR33","unstructured":"van\u00a0Noord G. FSA utilities toolbox. http:\/\/odur.let.rug.nl\/~vannoord\/Fsa\/"},{"key":"189_CR34","first-page":"472","volume-title":"TACAS","author":"M Veanes","year":"2012","unstructured":"Veanes M, Bj\u00f8rner N (2012) Symbolic automata: the toolkit. In: TACAS, pp 472\u2013477"},{"key":"189_CR35","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1145\/2103656.2103674","volume-title":"POPL","author":"M Veanes","year":"2012","unstructured":"Veanes M, Hooimeijer P, Livshits B, Molnar D, Bjorner N (2012) Symbolic finite state transducers: algorithms and applications. In: POPL, pp 137\u2013150"},{"key":"189_CR36","doi-asserted-by":"crossref","first-page":"32","DOI":"10.1145\/1250734.1250739","volume-title":"PLDI","author":"G Wassermann","year":"2007","unstructured":"Wassermann G, Su Z (2007) Sound and precise analysis of web applications for injection vulnerabilities. In: PLDI, pp 32\u201341"},{"key":"189_CR37","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1145\/1368088.1368112","volume-title":"ICSE","author":"G Wassermann","year":"2008","unstructured":"Wassermann G, Su Z (2008) Static detection of cross-site scripting vulnerabilities. In: ICSE, pp 171\u2013180"},{"key":"189_CR38","doi-asserted-by":"crossref","first-page":"249","DOI":"10.1145\/1390630.1390661","volume-title":"ISSTA","author":"G Wassermann","year":"2008","unstructured":"Wassermann G, Yu D, Chander A, Dhurjati D, Inamura H, Su Z (2008) Dynamic test input generation for web applications. In: ISSTA, pp 249\u2013260"},{"key":"189_CR39","first-page":"13","volume-title":"USENIX-SS","author":"Y Xie","year":"2006","unstructured":"Xie Y, Aiken A (2006) Static detection of security vulnerabilities in scripting languages. In: USENIX-SS, p 13"},{"key":"189_CR40","first-page":"154","volume-title":"TACAS","author":"F Yu","year":"2010","unstructured":"Yu F, Alkhalaf M, Bultan T (2010) Stranger: an automata-based string analysis tool for PHP. In: TACAS, pp 154\u2013157"},{"key":"189_CR41","doi-asserted-by":"crossref","first-page":"251","DOI":"10.1145\/1985793.1985828","volume-title":"ICSE","author":"F Yu","year":"2011","unstructured":"Yu F, Alkhalaf M, Bultan T (2011) Patching vulnerabilities with sanitization synthesis. In: ICSE, pp 251\u2013260"},{"key":"189_CR42","first-page":"306","volume-title":"SPIN","author":"F Yu","year":"2008","unstructured":"Yu F, Bultan T, Cova M, Ibarra OH (2008) Symbolic string verification: an automata-based approach. In: SPIN, pp 306\u2013324"},{"key":"189_CR43","first-page":"20","volume-title":"SPIN","author":"F Yu","year":"2011","unstructured":"Yu F, Bultan T, Hardekopf B (2011) String abstractions for string verification. In: SPIN, pp 20\u201337"},{"issue":"8","key":"189_CR44","doi-asserted-by":"crossref","first-page":"1909","DOI":"10.1142\/S0129054111009112","volume":"22","author":"F Yu","year":"2011","unstructured":"Yu F, Bultan T, Ibarra OH (2011) Relational string verification using multi-track automata. Int J Found Comput Sci 22(8):1909\u20131924","journal-title":"Int J Found Comput Sci"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-013-0189-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-013-0189-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-013-0189-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,3,5]],"date-time":"2022-03-05T13:38:32Z","timestamp":1646487512000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-013-0189-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,9,5]]},"references-count":44,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2014,2]]}},"alternative-id":["189"],"URL":"https:\/\/doi.org\/10.1007\/s10703-013-0189-1","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,9,5]]}}}