{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,29]],"date-time":"2026-01-29T22:46:25Z","timestamp":1769726785394,"version":"3.49.0"},"publisher-location":"Cham","reference-count":40,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319216898","type":"print"},{"value":"9783319216904","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","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":[[2015]]},"DOI":"10.1007\/978-3-319-21690-4_15","type":"book-chapter","created":{"date-parts":[[2015,7,15]],"date-time":"2015-07-15T06:08:27Z","timestamp":1436940507000},"page":"255-272","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":61,"title":["Automata-Based Model Counting for String Constraints"],"prefix":"10.1007","author":[{"given":"Abdulbaki","family":"Aydin","sequence":"first","affiliation":[]},{"given":"Lucas","family":"Bang","sequence":"additional","affiliation":[]},{"given":"Tevfik","family":"Bultan","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,7,16]]},"reference":[{"key":"15_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"150","DOI":"10.1007\/978-3-319-08867-9_10","volume-title":"Computer Aided Verification","author":"PA Abdulla","year":"2014","unstructured":"Abdulla, P.A., Atig, M.F., Chen, Y.-F., Hol\u00edk, L., Rezine, A., R\u00fcmmer, P., Stenman, J.: String constraints for verification. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 150\u2013166. Springer, Heidelberg (2014)"},{"key":"15_CR2","doi-asserted-by":"crossref","unstructured":"Alkhalaf, M., Aydin, A., Bultan, T.: Semantic differential repair for input validation and sanitization. In: Proceedings of the International Symposium on Software Testing and Analysis (ISSTA), pp. 225\u2013236 (2014)","DOI":"10.1145\/2610384.2610401"},{"key":"15_CR3","doi-asserted-by":"crossref","unstructured":"Alkhalaf, M., Bultan, T., Gallegos, J.L.: Verifying client-side input validation functions using string analysis. In: Proceedings of the 34th International Conference on Software Engineering (ICSE), pp. 947\u2013957 (2012)","DOI":"10.1109\/ICSE.2012.6227124"},{"issue":"4","key":"15_CR4","doi-asserted-by":"publisher","first-page":"605","DOI":"10.1142\/S0129054103001911","volume":"14","author":"C Bartzis","year":"2003","unstructured":"Bartzis, C., Bultan, T.: Efficient symbolic representations for arithmetic constraints in verification. Int. J. Found. Comput. Sci. 14(4), 605\u2013624 (2003)","journal-title":"Int. J. Found. Comput. Sci."},{"key":"15_CR5","volume-title":"Algebraic Graph Theory","author":"N Biggs","year":"1993","unstructured":"Biggs, N.: Algebraic Graph Theory. Cambridge University Press, Cambridge Mathematical Library, Cambridge (1993)"},{"key":"15_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/978-3-642-00768-2_27","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"N Bj\u00f8rner","year":"2009","unstructured":"Bj\u00f8rner, N., Tillmann, N., Voronkov, A.: Path feasibility analysis for string-manipulating programs. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 307\u2013321. Springer, Heidelberg (2009)"},{"key":"15_CR7","doi-asserted-by":"crossref","unstructured":"Borges, M., Filieri, A., d\u2019Amorim, M., Pasareanu, C.S., Visser, W.: Compositional solution space quantification for probabilistic software analysis. In: Proceedigns of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) (2014)","DOI":"10.1145\/2594291.2594329"},{"key":"15_CR8","unstructured":"BRICS. The MONA project. http:\/\/www.brics.dk\/mona\/"},{"key":"15_CR9","doi-asserted-by":"crossref","unstructured":"Christensen, A.S., M\u00f8ller, A., Schwartzbach, M.I.: Precise analysis of string expressions. In: Proceedings of the 10th International Static Analysis Symposium (SAS), pp. 1\u201318 (2003)","DOI":"10.1007\/3-540-44898-5_1"},{"issue":"3","key":"15_CR10","doi-asserted-by":"crossref","first-page":"321","DOI":"10.3233\/JCS-2007-15302","volume":"15","author":"D Clark","year":"2007","unstructured":"Clark, D., Hunt, S., Malacaria, P.: A static analysis for quantifying information flow in a simple imperative language. J. Comput. Secur. 15(3), 321\u2013371 (2007)","journal-title":"J. Comput. Secur."},{"key":"15_CR11","volume-title":"Introduction to Algorithms","author":"TH Cormen","year":"2001","unstructured":"Cormen, T.H., Stein, C., Rivest, R.L., Leiserson, C.E.: Introduction to Algorithms, 2nd edn. McGraw-Hill Higher Education, Boston (2001)","edition":"2"},{"key":"15_CR12","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":"15_CR13","doi-asserted-by":"crossref","unstructured":"Filieri, A., Pasareanu, C.S., Visser, W.: Reliability analysis in symbolic pathfinder. In: Proceedings of the 35th International Conference on Software Engineering (ICSE), pp. 622\u2013631 (2013)","DOI":"10.1109\/ICSE.2013.6606608"},{"key":"15_CR14","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511801655","volume-title":"Analytic Combinatorics","author":"P Flajolet","year":"2009","unstructured":"Flajolet, P., Sedgewick, R.: Analytic Combinatorics, 1st edn. Cambridge University Press, New York (2009)","edition":"1"},{"key":"15_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/978-3-642-39611-3_21","volume-title":"Hardware and Software: Verification and Testing","author":"V Ganesh","year":"2013","unstructured":"Ganesh, V., Minnes, M., Solar-Lezama, A., Rinard, M.: Word equations with length constraints: what\u2019s decidable? In: Biere, A., Nahir, A., Vos, T. (eds.) HVC. LNCS, vol. 7857, pp. 209\u2013226. Springer, Heidelberg (2013)"},{"key":"15_CR16","doi-asserted-by":"crossref","DOI":"10.1201\/b16132","volume-title":"Handbook of Graph Theory","author":"JL Gross","year":"2013","unstructured":"Gross, J.L., Yellen, J., Zhang, P.: Handbook of Graph Theory, 2nd edn. Chapman and Hall\/CRC, Boca Raton (2013)","edition":"2"},{"key":"15_CR17","unstructured":"Hooimeijer, P., Livshits, B., Molnar, D., Saxena, P., Veanes, M.: Fast and precise sanitizer analysis with bek. In: Proceedings of the 20th USENIX Conference on Security (2011)"},{"key":"15_CR18","doi-asserted-by":"crossref","unstructured":"Hooimeijer, P., Weimer, W.: A decision procedure for subset constraints over regular languages. In: Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pp. 188\u2013198 (2009)","DOI":"10.1145\/1543135.1542498"},{"key":"15_CR19","doi-asserted-by":"crossref","unstructured":"Hooimeijer, P., Weimer, W.: Solving string constraints lazily. In: Proceedings of the 25th IEEE\/ACM International Conference on Automated Software Engineering (ASE), pp. 377\u2013386 (2010)","DOI":"10.1145\/1858996.1859080"},{"key":"15_CR20","doi-asserted-by":"crossref","unstructured":"Kausler, S., Sherman, E.: Evaluation of string constraint solvers in the context of symbolic execution. In: Proceedings of the 29th ACM\/IEEE International Conference on Automated Software Engineering (ASE), pp. 259\u2013270 (2014)","DOI":"10.1145\/2642937.2643003"},{"key":"15_CR21","doi-asserted-by":"crossref","unstructured":"Kiezun, A., Ganesh, V., Guo, P.J., Hooimeijer, P., Ernst, M.D.: Hampi: a solver for string constraints. In: Proceedings of the 18th International Symposium on Software Testing and Analysis (ISSTA), pp. 105\u2013116 (2009)","DOI":"10.1145\/1572272.1572286"},{"key":"15_CR22","volume-title":"The Art of Computer Programming, Volume 1: Fundamental Algorithms","author":"DE Knuth","year":"1968","unstructured":"Knuth, D.E.: The Art of Computer Programming, Volume 1: Fundamental Algorithms. Addison-Wesley, Reading (1968)"},{"key":"15_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/978-3-319-03077-7_2","volume-title":"Hardware and Software: Verification and Testing","author":"G Li","year":"2013","unstructured":"Li, G., Ghosh, I.: PASS: string solving with parameterized array and interval automaton. In: Bertacco, V., Legay, A. (eds.) HVC 2013. LNCS, vol. 8244, pp. 15\u201331. Springer, Heidelberg (2013)"},{"key":"15_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"646","DOI":"10.1007\/978-3-319-08867-9_43","volume-title":"Computer Aided Verification","author":"T Liang","year":"2014","unstructured":"Liang, T., Reynolds, A., Tinelli, C., Barrett, C., Deters, M.: A DPLL(T) Theory solver for a theory of strings and regular expressions. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 646\u2013662. Springer, Heidelberg (2014)"},{"key":"15_CR25","doi-asserted-by":"crossref","unstructured":"Luu, L., Shinde, S., Saxena, P., Demsky, B.: A model counter for constraints over unbounded strings. In: Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), p. 57 (2014)","DOI":"10.1145\/2594291.2594331"},{"key":"15_CR26","doi-asserted-by":"crossref","unstructured":"McCamant, S., Ernst, M.D.: Quantitative information flow as network flow capacity. In: Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pp. 193\u2013205 (2008)","DOI":"10.1145\/1379022.1375606"},{"issue":"6","key":"15_CR27","doi-asserted-by":"publisher","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. SIGSOFT Softw. Eng. Notes 37(6), 1\u20135 (2012)","journal-title":"SIGSOFT Softw. Eng. Notes"},{"key":"15_CR28","doi-asserted-by":"crossref","unstructured":"Saxena, P., Akhawe, D., Hanna, S., Mao, F., McCamant, S., Song, D.: A symbolic execution framework for javascript. In: Proceedings of the 31st IEEE Symposium on Security and Privacy (2010)","DOI":"10.1109\/SP.2010.38"},{"key":"15_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"288","DOI":"10.1007\/978-3-642-00596-1_21","volume-title":"Foundations of Software Science and Computational Structures","author":"G Smith","year":"2009","unstructured":"Smith, G.: On the foundations of quantitative information flow. In: de Alfaro, L. (ed.) FOSSACS 2009. LNCS, vol. 5504, pp. 288\u2013302. Springer, Heidelberg (2009)"},{"key":"15_CR30","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139058520","volume-title":"Enumerative Combinatorics: vol. 1","author":"RP Stanley","year":"2011","unstructured":"Stanley, R.P.: Enumerative Combinatorics: vol. 1, 2nd edn. Cambridge University Press, New York (2011)","edition":"2"},{"key":"15_CR31","doi-asserted-by":"crossref","unstructured":"Tateishi, T., Pistoia, M., Tripp, O.: Path- and index-sensitive string analysis based on monadic second-order logic. In: Proceedings of the International Symposium on Software Testing and Analysis (ISSTA), pp. 166\u2013176 (2011)","DOI":"10.1145\/2001420.2001441"},{"key":"15_CR32","doi-asserted-by":"crossref","unstructured":"Trinh, M.-T., Chu, D.-H., Jaffar, J.: S3: a symbolic string solver for vulnerability detection in web applications. In: Proceedings of the ACM SIGSAC Conference on Computer and Communications Security (CCS), pp. 1232\u20131243 (2014)","DOI":"10.1145\/2660267.2660372"},{"key":"15_CR33","unstructured":"Wolfram Research Inc., Mathematica (2014). http:\/\/www.wolfram.com\/mathematica\/"},{"key":"15_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-46419-0_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P Wolper","year":"2000","unstructured":"Wolper, P., Boigelot, B.: On the construction of automata from linear arithmetic constraints. In: Graf, S. (ed.) TACAS 2000. LNCS, vol. 1785, pp. 1\u201319. Springer, Heidelberg (2000)"},{"key":"15_CR35","unstructured":"Yu, F.: Automatic verification of string manipulating programs. Ph.D. thesis. University of California, Santa Barbara (2010)"},{"key":"15_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/978-3-642-12002-2_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"F Yu","year":"2010","unstructured":"Yu, F., Alkhalaf, M., Bultan, T.: Stranger: an automata-based string analysis tool for PHP. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 154\u2013157. Springer, Heidelberg (2010)"},{"key":"15_CR37","doi-asserted-by":"crossref","unstructured":"Yu, F., Alkhalaf, M., Bultan, T.: Patching vulnerabilities with sanitization synthesis. In: Proceedings of the 33rd International Conference on Software Engineering (ICSE), pp. 131\u2013134 (2011)","DOI":"10.1145\/1985793.1985828"},{"issue":"1","key":"15_CR38","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1007\/s10703-013-0189-1","volume":"44","author":"Y Fang","year":"2014","unstructured":"Fang, Y., Alkhalaf, M., Bultan, T., Ibarra, O.H.: Automata-based symbolic string analysis for vulnerability detection. Formal Methods Syst. Des. 44(1), 44\u201370 (2014)","journal-title":"Formal Methods Syst. Des."},{"key":"15_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"306","DOI":"10.1007\/978-3-540-85114-1_21","volume-title":"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: Havelund, K., Majumdar, R. (eds.) SPIN 2008. LNCS, vol. 5156, pp. 306\u2013324. Springer, Heidelberg (2008)"},{"key":"15_CR40","doi-asserted-by":"crossref","unstructured":"Zheng, Y., Zhang, X., Ganesh, V.: Z3-str: a z3-based string solver for web application analysis. In: Proceedings of the 9th Joint Meeting on Foundations of Software Engineering (ESEC\/FSE), pp. 114\u2013124 (2013)","DOI":"10.1145\/2491411.2491456"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-21690-4_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,9,5]],"date-time":"2020-09-05T01:26:58Z","timestamp":1599269218000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-21690-4_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319216898","9783319216904"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-21690-4_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"16 July 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}