一句话：提出 SymMC，借助对称信息对 Alloy 规约做近似模型枚举与计数。
该论文关注 Alloy 规约分析中的模型枚举与计数问题。Alloy 提供一阶关系逻辑用于书写软件系统关键性质规约，并配有全自动分析后端，已广泛应用于验证、安全与合成等领域。随着模型空间增大，精确枚举或计数所有模型往往代价高昂。SymMC 的核心思路是利用规约中蕴含的对称信息来压缩搜索空间，从而对 Alloy 规约进行近似的模型枚举与计数。标题与摘要表明该工作面向 Alloy 规约，强调对称性在模型枚举与计数中的作用；但给出的摘要未提供具体算法细节、实验设置及定量结果。
Specifying and analyzing critical properties of software systems plays an important role in the development of reliable systems. Alloy is a mature tool-set that provides a first-order relational logic for writing specifications, and a fully automatic powerful backend for analyzing the specifications. It has been widely applied in areas including verification, security, and synthesis.
@inproceedings{paperbot7043,
title = {SymMC: approximate model enumeration and counting using symmetry information for Alloy specifications},
author = {Wenxi Wang and Yang Hu and Kenneth L. McMillan and Sarfraz Khurshid},
booktitle = {FSE},
year = {2022},
doi = {10.1145/3540250.3549161}
}