Model counting for recursively-defined strings Conference Paper


Author(s): Trinh, Minh-Thai; Chu, Duc-Hiep; Jaffar, Joxan
Title: Model counting for recursively-defined strings
Title Series: LNCS
Affiliation IST Austria
Abstract: 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.
Conference Title: CAV: Computer Aided Verification
Volume: 10427
Conference Dates: July 22 - 28, 2017
Conference Location: Heidelberg, Germany
Publisher: Springer  
Date Published: 2017-01-01
Start Page: 399
End Page: 418
Sponsor: Austrian Science Fund (FWF) under grants S11402-N23 (RiSE/SHiNE) and Z211-N23 (Wittgenstein Award)
DOI: 10.1007/978-3-319-63390-9_21
Open access: no
IST Austria Authors
  1. Duc-Hiep Chu
    3 Chu
Related IST Austria Work