SymMC: approximate model enumeration and counting using symmetry information for Alloy specifications
Abstract
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.
BibTeX
@inproceedings{Wang-al:FSE22,
author = {Wenxi Wang and
Yang Hu and
Kenneth L. McMillan and
Sarfraz Khurshid},
title = {{SymMC:} approximate model enumeration and counting using symmetry information for Alloy specifications},
booktitle = {{ESEC/SIGSOFT} {FSE}},
pages = {1209--1220},
publisher = {{ACM}},
year = {2022},
}