AlloyMC: Alloy meets model counting
AlloyMC: Alloy meets model counting
复制标题
AlloyMC：合金与模型计数的结合
DOI：
10.1145/3368089.3417938
复制
发表时间：
2020
期刊：
影响因子：
--
通讯作者：
Khurshid, Sarfraz
中科院分区：
文献类型：
--
作者：
Yang, Jiayi;Wang, Wenxi;Marinov, Darko;Khurshid, Sarfraz
软件系统期望属性的识别和分析在开发更可靠的系统中起着重要的作用。Alloy是一个成熟的工具集，它提供了一个一阶关系逻辑，具有用于编写规范的传递闭包，以及一个基于命题可满足性（SAT）求解器的全自动后端，用于分析它们。Alloy直观的符号和对现代求解器的支持使其成为一种特别有效的规范和分析工具，已应用于多个领域，包括验证，安全和综合。本文介绍了Alloy的一个新后端，它补充了SAT求解器，并提供了一种新的方法来帮助Alloy用户更有效地使用工具集，特别是在需要对同一公式进行多个解决方案的情况下。我们为Alloy后端添加了对模型计数的支持，即，计算给定公式的解的个数。我们扩展了Alloy文法，增加了一个新的模型计数命令，并扩展了Alloy GUI，实现了AlloyMC，支持两个最先进的模型计数器：近似模型计数器ApproxMC和精确模型计数器ProjMC。AlloyMC可在Linux、Mac和Windows上运行。要使用AlloyMC，用户只需下载并运行其集成的JavaScript文件，而无需安装依赖项（例如，模型计数器及其依赖库）。AlloyMC的源代码、数据库文件和数据集都是公开的。
Specifying and analyzing desired properties of software systems can play an important role in the development of more dependable systems. Alloy is a mature tool-set that provides a first-order, rela- tional logic with transitive closure for writing the specifications, and a fully automatic backend based on propositional satisfiability (SAT) solvers for analyzing them. Alloy’s intuitive notation and sup- port for modern solvers make it a particularly effective specification and analysis tool, which has been applied in several domains, including verification, security, and synthesis. This paper introduces a new backend for Alloy, which complements SAT solvers, and provides a new method to assist Alloy users to more effectively use the tool-set, specifically in scenarios where multiple solutions to the same formula are desired. We add to the Alloy backend support for model counting, i.e., computing the number of solutions to the given formula. We extend the Alloy grammar to add a new com- mand for model counting, and extend the Alloy GUI to customize it. Our implementation, called AlloyMC, supports two state-of-the-art model counters: the approximate model counter ApproxMC and the exact model counter ProjMC. AlloyMC runs on Linux, Mac, and Windows. To use AlloyMC, users just download and run its integrated JAR file with no need to install dependencies (e.g., model counters and their dependent libraries). The AlloyMC source code, the JAR file, and the data set are available publicly.
登录
查看更多内容
用于模型计数和定量程序分析的子公式缓存
DOI：
10.1109/ase.2019.00050
发表时间：
2019
期刊：
2019 34th IEEE/ACM International Conference on Automated Software Engineering (ASE
影响因子：
--
作者：
Eiers, William;Saha, Seemanta;Brennan, Tegan;Bultan, Tevfik
通讯作者：
Bultan, Tevfik
通过加权模型集成进行混合域中的概率推理
DOI：
--
发表时间：
2015
期刊：
International Joint Conference on Artificial Intelligence
影响因子：
--
作者：
Vaishak Belle;A. Passerini;Guy Van den Broeck
通讯作者：
Guy Van den Broeck
影响因子：
7.4
作者：
E. Uzuncaova;S. Khurshid;D. Batory
通讯作者：
D. Batory
BIRD：设计高效的 CNF-XOR SAT 求解器及其在近似模型计数中的应用
DOI：
--
发表时间：
2019
期刊：
AAAI Conference on Artificial Intelligence
影响因子：
--
作者：
M. Soos;Kuldeep S. Meel
通讯作者：
Kuldeep S. Meel
DOI：
10.1007/978-3-319-57288-8_9
发表时间：
2017
期刊：
IACR Cryptol. ePrint Arch.
影响因子：
--
作者：
Mateus Borges;Quoc;A. Filieri;C. Păsăreanu
通讯作者：
C. Păsăreanu