TY - GEN
T1 - Parameterized model counting for string and numeric constraints
AU - Aydin, Abdulbaki
AU - Eiers, William
AU - Bang, Lucas
AU - Brennan, Tegan
AU - Gavrilov, Miroslav
AU - Bultan, Tevfik
AU - Yu, Fang
N1 - Publisher Copyright:
© 2018 Association for Computing Machinery.
PY - 2018/10/26
Y1 - 2018/10/26
N2 - Recently, symbolic program analysis techniques have been extended to quantitative analyses using model counting constraint solvers. Given a constraint and a bound, a model counting constraint solver computes the number of solutions for the constraint within the bound. We present a parameterized model counting constraint solver for string and numeric constraints. We first construct a multi-track deterministic finite state automaton that accepts all solutions to the given constraint. We limit the numeric constraints to linear integer arithmetic, and for non-regular string constraints we over-approximate the solution set. Counting the number of accepting paths in the generated automaton 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 experimentally demonstrate the effectiveness of our approach on a large set of string and numeric constraints extracted from software applications. We experimentally compare our tool to five existing model counting constraint solvers for string and numeric constraints and demonstrate that our tool is as efficient and as or more precise than other solvers. Moreover, our tool can handle mixed constraints with string and integer variables that no other tool can.
AB - Recently, symbolic program analysis techniques have been extended to quantitative analyses using model counting constraint solvers. Given a constraint and a bound, a model counting constraint solver computes the number of solutions for the constraint within the bound. We present a parameterized model counting constraint solver for string and numeric constraints. We first construct a multi-track deterministic finite state automaton that accepts all solutions to the given constraint. We limit the numeric constraints to linear integer arithmetic, and for non-regular string constraints we over-approximate the solution set. Counting the number of accepting paths in the generated automaton 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 experimentally demonstrate the effectiveness of our approach on a large set of string and numeric constraints extracted from software applications. We experimentally compare our tool to five existing model counting constraint solvers for string and numeric constraints and demonstrate that our tool is as efficient and as or more precise than other solvers. Moreover, our tool can handle mixed constraints with string and integer variables that no other tool can.
KW - Model counting
KW - constraint solving
KW - quantitative program analysis
UR - http://www.scopus.com/inward/record.url?scp=85058286556&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85058286556&partnerID=8YFLogxK
U2 - 10.1145/3236024.3236064
DO - 10.1145/3236024.3236064
M3 - Conference contribution
AN - SCOPUS:85058286556
T3 - ESEC/FSE 2018 - Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering
SP - 400
EP - 410
BT - ESEC/FSE 2018 - Proceedings of the 2018 26th ACM Joint Meeting on European So ftware Engineering Conference and Symposium on the Foundations of So ftware Engineering
A2 - Garci, Alessandro
A2 - Pasareanu, Corina S.
A2 - Leavens, Gary T.
T2 - 26th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/FSE 2018
Y2 - 4 November 2018 through 9 November 2018
ER -