Parameterized Model Counting for String and Numeric Constraints

Recently, symbolic program analysis techniques have been
extended to quantitative and probabilistic program analyses using model
counting constraint solvers. Given a constraint and a bound, a model
counting constraint solver returns the number of solutions for the given
constraint within the given bound. In this paper, we present a parameter-
ized model counting constraint solver for string and numeric constraints.
Given a constraint over strings and integers, we first generate automata
that accept all solutions to the given constraint. We limit the numeric
constraints to linear integer arithmetic, and for non-regular string con-
straints we over-approximate the solution set. Counting the number of
accepting paths in the generated automata solves the model counting
problem. Our approach is parameterized in the sense that, we do not
assume a finite domain size during automata construction, resulting in
a potentially infinite set of solutions, and our model counting approach
works for arbitrarily large bounds. We demonstrate the effectiveness of
our approach on a large set of string and numeric constraints extracted
from software applications.