SymMC: approximate model enumeration and counting using symmetry information for Alloy specifications
Wenxi Wang, Hu Yang, Kenneth L. McMillan, Sarfraz Khurshid · Proceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering · 2022
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.