--- _id: '962' abstract: - lang: eng text: 'We present a new algorithm for model counting of a class of string constraints. In addition to the classic operation of concatenation, our class includes some recursively defined operations such as Kleene closure, and replacement of substrings. Additionally, our class also includes length constraints on the string expressions, which means, by requiring reasoning about numbers, that we face a multi-sorted logic. In the end, our string constraints are motivated by their use in programming for web applications. Our algorithm comprises two novel features: the ability to use a technique of (1) partial derivatives for constraints that are already in a solved form, i.e. a form where its (string) satisfiability is clearly displayed, and (2) non-progression, where cyclic reasoning in the reduction process may be terminated (thus allowing for the algorithm to look elsewhere). Finally, we experimentally compare our model counter with two recent works on model counting of similar constraints, SMC [18] and ABC [5], to demonstrate its superior performance.' alternative_title: - LNCS article_processing_charge: No author: - first_name: Minh full_name: Trinh, Minh last_name: Trinh - first_name: Duc Hiep full_name: Chu, Duc Hiep id: 3598E630-F248-11E8-B48F-1D18A9856A87 last_name: Chu - first_name: Joxan full_name: Jaffar, Joxan last_name: Jaffar citation: ama: 'Trinh M, Chu DH, Jaffar J. Model counting for recursively-defined strings. In: Majumdar R, Kunčak V, eds. Vol 10427. Springer; 2017:399-418. doi:10.1007/978-3-319-63390-9_21' apa: 'Trinh, M., Chu, D. H., & Jaffar, J. (2017). Model counting for recursively-defined strings. In R. Majumdar & V. Kunčak (Eds.) (Vol. 10427, pp. 399–418). Presented at the CAV: Computer Aided Verification, Heidelberg, Germany: Springer. https://doi.org/10.1007/978-3-319-63390-9_21' chicago: Trinh, Minh, Duc Hiep Chu, and Joxan Jaffar. “Model Counting for Recursively-Defined Strings.” edited by Rupak Majumdar and Viktor Kunčak, 10427:399–418. Springer, 2017. https://doi.org/10.1007/978-3-319-63390-9_21. ieee: 'M. Trinh, D. H. Chu, and J. Jaffar, “Model counting for recursively-defined strings,” presented at the CAV: Computer Aided Verification, Heidelberg, Germany, 2017, vol. 10427, pp. 399–418.' ista: 'Trinh M, Chu DH, Jaffar J. 2017. Model counting for recursively-defined strings. CAV: Computer Aided Verification, LNCS, vol. 10427, 399–418.' mla: Trinh, Minh, et al. Model Counting for Recursively-Defined Strings. Edited by Rupak Majumdar and Viktor Kunčak, vol. 10427, Springer, 2017, pp. 399–418, doi:10.1007/978-3-319-63390-9_21. short: M. Trinh, D.H. Chu, J. Jaffar, in:, R. Majumdar, V. Kunčak (Eds.), Springer, 2017, pp. 399–418. conference: end_date: 2017-07-28 location: Heidelberg, Germany name: 'CAV: Computer Aided Verification' start_date: 2017-07-24 date_created: 2018-12-11T11:49:26Z date_published: 2017-01-01T00:00:00Z date_updated: 2023-09-22T09:58:02Z day: '01' department: - _id: ToHe doi: 10.1007/978-3-319-63390-9_21 editor: - first_name: Rupak full_name: Majumdar, Rupak last_name: Majumdar - first_name: Viktor full_name: Kunčak, Viktor last_name: Kunčak external_id: isi: - '000431900900021' intvolume: ' 10427' isi: 1 language: - iso: eng month: '01' oa_version: None page: 399 - 418 project: - _id: 25F5A88A-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11402-N23 name: Moderne Concurrency Paradigms - _id: 25F42A32-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: Z211 name: The Wittgenstein Prize publication_identifier: issn: - '03029743' publication_status: published publisher: Springer publist_id: '6443' quality_controlled: '1' scopus_import: '1' status: public title: Model counting for recursively-defined strings type: conference user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1 volume: 10427 year: '2017' ...