一句话：提出面向字符串与数值约束的参数化模型计数求解器，用多轨 DFA 计数解，支持任意大界与混合约束。
符号程序分析已借助模型计数约束求解器扩展到定量分析。给定约束与界，模型计数求解器计算界内解数。本文提出面向字符串与数值约束的参数化模型计数求解器。方法先构造接受约束解集的多轨确定性有限自动机：数值约束限于线性整数算术，非正则字符串约束则过近似。通过计数自动机中接受路径数求解模型计数。该方法不假定有限域大小，构造自动机时解集可无限，计数适用于任意大界。实验在软件应用中提取的大量字符串与数值约束上进行，与五个现有求解器比较，工具效率相当、精度不低于其他工具，且能处理无其他工具支持的字符串-整数混合约束。
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.
@inproceedings{paperbot4664,
title = {Parameterized model counting for string and numeric constraints},
author = {Abdulbaki Aydin and William Eiers and Lucas Bang and Tegan Brennan and Miroslav Gavrilov and Tevfik Bultan and Fang Yu},
booktitle = {FSE},
year = {2018},
doi = {10.1145/3236024.3236064}
}