Write a Blog >>
Fri 13 Nov 2020 01:30 - 01:32 at Virtual room 2 - SAT and Synthesis

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.

Fri 13 Nov
Times are displayed in time zone: (UTC) Coordinated Universal Time change

01:30 - 02:00: SAT and SynthesisPaper Presentations / Research Papers / Tool Demos at Virtual room 2
01:30 - 01:32
Talk
Tool Demos
Jiayi YangUniversity of Texas at Austin, USA, Wenxi WangUniversity of Texas at Austin, USA, Darko MarinovUniversity of Illinois at Urbana-Champaign, Sarfraz KhurshidUniversity of Texas at Austin
DOI
01:32 - 01:34
Talk
Research Papers
Zifan NanNorth Carolina State University, USA, Hui GuanUniversity of Massachusetts at Amherst, USA, Xipeng ShenNorth Carolina State University, USA
DOI
01:35 - 01:36
Talk
Research Papers
Shivam HandaMassachusetts Institute of Technology, USA, Martin RinardMassachusetts Institute of Technology, USA
DOI
01:37 - 01:38
Talk
Tool Demos
Abtin MolaviHarvey Mudd College, USA, Mara DowningHarvey Mudd College, USA, Tommy SchneiderHarvey Mudd College, USA, Lucas BangHarvey Mudd College
DOI
01:39 - 01:40
Talk
Tool Demos
Xie Li, Yi LiNanyang Technological University, Singapore, Yong LiInstitute of Software, Chinese Academy of Sciences, Xuechao SunInstitute of Software at Chinese Academy of Sciences, China, Andrea TurriniState Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Lijun ZhangInstitute of Software, Chinese Academy of Sciences
DOI
01:41 - 02:00
Talk
Paper Presentations
Abtin MolaviHarvey Mudd College, USA, Jiayi YangUniversity of Texas at Austin, USA, Lucas BangHarvey Mudd College, Xie Li, Zifan NanNorth Carolina State University, USA, Shivam HandaMassachusetts Institute of Technology, USA, M: Abhik RoychoudhuryNational University of Singapore, Singapore