一句话：提出 MCBAT 工具，将有界整数数组约束归约到 LIA，并用 Barvinok 算法进行模型计数。
本文面向自动定量程序分析中对数据结构进行模型计数的需求，提出了实用工具 MCBAT。MCBAT 处理所有数组长度有限的有界整数数组上的量化约束。其核心方法是将数组理论归约到未解释函数与线性整数算术（LIA），进而利用 Barvinok 的多项式时间整数格点枚举算法完成模型计数。作者还通过一个案例研究展示了该工具在自动定量程序分析中的适用性。MCBAT 以 Docker 镜像形式提供，可立即使用，源代码也在 GitHub 仓库中公开。
Model counting procedures for data structures are crucial for advancing the field of automated quantitative program analysis. We present a tool for Model Counting for Bounded Array Theory (MCBAT). MCBAT works on quantified integer array constraints in which all arrays have a finite length. We employ reductions from the theory of arrays to uninterpreted functions and linear integer arithmetic (LIA). Once reduced to LIA, we leverage Barvinok's polynomial time integer lattice point enumeration algorithm. Finally, we present a case study demonstrating applicability to automated quantitative program analysis. MCBAT is available for immediate use as a Docker image and the source code is freely available in our Github repository.
DOI 原文 ·
@inproceedings{paperbot5840,
title = {MCBAT: a practical tool for model counting constraints on bounded integer arrays},
author = {Abtin Molavi and Mara Downing and Tommy Schneider and Lucas Bang},
booktitle = {FSE},
year = {2020},
doi = {10.1145/3368089.3417937}
}