AlloyMC: Alloy meets model counting

Jiayi Yang, Wenxi Wang, Darko Marinov, Sarfraz Khurshid

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.

Original languageEnglish (US)
Title of host publicationESEC/FSE 2020 - Proceedings of the 28th ACM Joint Meeting European Software Engineering Conference and Symposium on the Foundations of Software Engineering
EditorsPrem Devanbu, Myra Cohen, Thomas Zimmermann
PublisherAssociation for Computing Machinery, Inc
Pages1541-1545
Number of pages5
ISBN (Electronic)9781450370431
DOIs
StatePublished - Nov 8 2020
Event28th ACM Joint Meeting European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/FSE 2020 - Virtual, Online, United States
Duration: Nov 8 2020Nov 13 2020

Publication series

NameESEC/FSE 2020 - Proceedings of the 28th ACM Joint Meeting European Software Engineering Conference and Symposium on the Foundations of Software Engineering

Conference

Conference28th ACM Joint Meeting European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/FSE 2020
CountryUnited States
CityVirtual, Online
Period11/8/2011/13/20

Keywords

  • Alloy
  • Model counting

ASJC Scopus subject areas

  • Software

Fingerprint Dive into the research topics of 'AlloyMC: Alloy meets model counting'. Together they form a unique fingerprint.

Cite this