{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T17:05:04Z","timestamp":1751648704598,"version":"3.40.3"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319633893"},{"type":"electronic","value":"9783319633909"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-63390-9_21","type":"book-chapter","created":{"date-parts":[[2017,7,12]],"date-time":"2017-07-12T08:53:50Z","timestamp":1499849630000},"page":"399-418","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":14,"title":["Model Counting for Recursively-Defined Strings"],"prefix":"10.1007","author":[{"given":"Minh-Thai","family":"Trinh","sequence":"first","affiliation":[]},{"given":"Duc-Hiep","family":"Chu","sequence":"additional","affiliation":[]},{"given":"Joxan","family":"Jaffar","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,7,13]]},"reference":[{"key":"21_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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., Holk, 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, Cham (2014). doi:10.1007\/978-3-319-08867-9_10"},{"key":"21_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"462","DOI":"10.1007\/978-3-319-21690-4_29","volume-title":"Computer Aided Verification","author":"PA Abdulla","year":"2015","unstructured":"Abdulla, P.A., Atig, M.F., Chen, Y.-F., Holk, L., Rezine, A., R\u00fcmmer, P., Stenman, J.: Norn: an SMT solver for string constraints. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 462\u2013469. Springer, Cham (2015). doi:10.1007\/978-3-319-21690-4_29"},{"key":"21_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/978-3-642-23082-0_8","volume-title":"Foundations of Security Analysis and Design VI","author":"MS Alvim","year":"2011","unstructured":"Alvim, M.S., Andr\u00e9s, M.E., Chatzikokolakis, K., Palamidessi, C.: Quantitative information flow and applications to differential privacy. In: Aldini, A., Gorrieri, R. (eds.) FOSAD 2011. LNCS, vol. 6858, pp. 211\u2013230. Springer, Heidelberg (2011). doi:10.1007\/978-3-642-23082-0_8"},{"issue":"2","key":"21_CR4","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1016\/0304-3975(95)00182-4","volume":"155","author":"V Antimirov","year":"1996","unstructured":"Antimirov, V.: Partial derivatives of regular expressions and finite automaton constructions. Theoret. Comput. Sci. 155(2), 291\u2013319 (1996)","journal-title":"Theoret. Comput. Sci."},{"key":"21_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/978-3-319-21690-4_15","volume-title":"Computer Aided Verification","author":"A Aydin","year":"2015","unstructured":"Aydin, A., Bang, L., Bultan, T.: Automata-based model counting for string constraints. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 255\u2013272. Springer, Cham (2015). doi:10.1007\/978-3-319-21690-4_15"},{"key":"21_CR6","doi-asserted-by":"crossref","unstructured":"Backes, M., K\u00f6pf, B., Rybalchenko, A.: Automatic discovery and quantification of information leaks. In: 2009 30th IEEE Symposium on Security and Privacy, pp. 141\u2013153, May 2009","DOI":"10.1109\/SP.2009.18"},{"key":"21_CR7","doi-asserted-by":"crossref","unstructured":"Bang, L., Aydin, A., Phan, Q.-S., Pasareanu, C.S., Bultan, T.: String analysis for side channels with segmented oracles. In: FSE, pp. 193\u2013204 (2016)","DOI":"10.1145\/2950290.2950362"},{"key":"21_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"702","DOI":"10.1007\/978-3-642-39799-8_49","volume-title":"Computer Aided Verification","author":"F Biondi","year":"2013","unstructured":"Biondi, F., Legay, A., Traonouez, L.-M., W\u0105sowski, A.: QUAIL: a quantitative security analyzer for imperative code. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 702\u2013707. Springer, Heidelberg (2013). doi:10.1007\/978-3-642-39799-8_49"},{"key":"21_CR9","doi-asserted-by":"crossref","unstructured":"Borges, M., Filieri, A., d\u2019Amorim, M., P\u0103s\u0103reanu, C.S., Visser, W.: Compositional solution space quantification for probabilistic software analysis. In: Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2014, pp. 123\u2013132. ACM, New York (2014)","DOI":"10.1145\/2594291.2594329"},{"issue":"2\u20134","key":"21_CR10","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1016\/j.ic.2007.07.003","volume":"206","author":"K Chatzikokolakis","year":"2008","unstructured":"Chatzikokolakis, K., Palamidessi, C., Panangaden, P.: Anonymity protocols as noisy channels. Inf. Comput. 206(2\u20134), 378\u2013401 (2008)","journal-title":"Inf. Comput."},{"issue":"3","key":"21_CR11","doi-asserted-by":"publisher","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":"21_CR12","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.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). doi:10.1007\/978-3-540-78800-3_24"},{"key":"21_CR13","doi-asserted-by":"crossref","unstructured":"Filieri, A., P\u0103s\u0103reanu, C.S., Visser, W.: Reliability analysis in symbolic pathfinder. In: Proceedings of the 2013 International Conference on Software Engineering, ICSE 2013, Piscataway, NJ, USA, pp. 622\u2013631. IEEE Press (2013)","DOI":"10.1109\/ICSE.2013.6606608"},{"key":"21_CR14","doi-asserted-by":"crossref","unstructured":"Kausler, S., Sherman, E.: Evaluation of string constraint solvers in the context of symbolic execution. In: ASE, pp. 259\u2013270 (2014)","DOI":"10.1145\/2642937.2643003"},{"key":"21_CR15","doi-asserted-by":"crossref","unstructured":"Kiezun, A., Ganesh, V., Guo, P.J., Hooimeijer, P., Ernst, M.D.: Hampi: a solver for string constraints. In: ISSTA, pp. 105\u2013116. ACM (2009)","DOI":"10.1145\/1572272.1572286"},{"key":"21_CR16","doi-asserted-by":"crossref","unstructured":"K\u00f6pf, B., Basin, D.: An information-theoretic model for adaptive side-channel attacks. In: Proceedings of the 14th ACM Conference on Computer and Communications Security, CCS 2007, pp. 286\u2013296. ACM, New York (2007)","DOI":"10.1145\/1315245.1315282"},{"key":"21_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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, Cham (2014). doi:10.1007\/978-3-319-08867-9_43"},{"key":"21_CR18","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 35th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2014, pp. 565\u2013576. ACM, New York (2014)","DOI":"10.1145\/2594291.2594331"},{"key":"21_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"410","DOI":"10.1007\/11814948_37","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"A Morgado","year":"2006","unstructured":"Morgado, A., Matos, P., Manquinho, V., Marques-Silva, J.: Counting models in integer domains. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 410\u2013423. Springer, Heidelberg (2006). doi:10.1007\/11814948_37"},{"key":"21_CR20","unstructured":"OWASP: Top ten project, May 2013. http:\/\/www.owasp.org\/"},{"issue":"6","key":"21_CR21","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"},{"issue":"1","key":"21_CR22","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1109\/JSAC.2002.806121","volume":"21","author":"A Sabelfeld","year":"2006","unstructured":"Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE J. Sel. A. Commun. 21(1), 5\u201319 (2006)","journal-title":"IEEE J. Sel. A. Commun."},{"key":"21_CR23","doi-asserted-by":"crossref","unstructured":"Saxena, P., Akhawe, D., Hanna, S., Mao, F., McCamant, S., Song, D.: A symbolic execution framework for JavaScript. In: SP, pp. 513\u2013528 (2010)","DOI":"10.1109\/SP.2010.38"},{"key":"21_CR24","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: Alfaro, L. (ed.) FoSSaCS 2009. LNCS, vol. 5504, pp. 288\u2013302. Springer, Heidelberg (2009). doi:10.1007\/978-3-642-00596-1_21"},{"key":"21_CR25","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: ACM-CCS, pp. 1232\u20131243. ACM (2014)","DOI":"10.1145\/2660267.2660372"},{"key":"21_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"218","DOI":"10.1007\/978-3-319-41528-4_12","volume-title":"Computer Aided Verification","author":"M-T Trinh","year":"2016","unstructured":"Trinh, M.-T., Chu, D.-H., Jaffar, J.: Progressive reasoning over recursively-defined strings. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 218\u2013240. Springer, Cham (2016). doi:10.1007\/978-3-319-41528-4_12"},{"key":"21_CR27","unstructured":"Trinh, M.-T., Chu, D.-H., Jaffar, J.: Technical report (2017). http:\/\/www.comp.nus.edu.sg\/~trinhmt\/"},{"key":"21_CR28","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1016\/0304-3975(92)00011-F","volume":"125","author":"S Yu","year":"1994","unstructured":"Yu, S., Zhuang, Q., Salomaa, K.: The state complexities of some basic operations on regular languages. Theor. Comput. Sci. 125, 315\u2013328 (1994)","journal-title":"Theor. Comput. Sci."},{"key":"21_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/978-3-319-21690-4_14","volume-title":"Computer Aided Verification","author":"Y Zheng","year":"2015","unstructured":"Zheng, Y., Ganesh, V., Subramanian, S., Tripp, O., Dolby, J., Zhang, X.: Effective search-space pruning for solvers of string equations, regular expressions and length constraints. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 235\u2013254. Springer, Cham (2015). doi:10.1007\/978-3-319-21690-4_14"},{"key":"21_CR30","doi-asserted-by":"crossref","unstructured":"Zheng, Y., Zhang, X., Ganesh, V.: Z3-str: a z3-based string solver for web application analysis. In: 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":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-63390-9_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,13]],"date-time":"2021-07-13T00:11:04Z","timestamp":1626135064000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-63390-9_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319633893","9783319633909"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-63390-9_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"13 July 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Heidelberg","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2017","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 July 2017","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 July 2017","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2017","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/cavconference.org\/2017\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}