Solution Enumeration Abstraction: A Modeling Idiom to Enhance a Lightweight Formal Method

Allison Sullivan, Darko Marinov, Sarfraz Khurshid

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

Abstract

Formal methods are a key to engineering more reliable systems. In this paper, we focus on an important application of formal methods — enumerating solutions to logical formulas that encode properties of interest. Solution enumeration has many uses, e.g., in systematic software testing, model counting, or hardware analysis. We introduce solution enumeration abstraction, a novel idiom that allows users to define data abstractions to enhance solution enumeration by specifying how the solutions must differ, so enumeration creates a high quality set of solutions of a manageable size. We embody the idiom as a technique built on top of Alloy, a well-known lightweight formal method, which is comprised of a first-order relational logic with transitive closure, and a SAT-based analysis engine. Experimental results show that our technique supports a variety of data abstractions, and can substantially reduce the number of solutions enumerated and the time to enumerate them.

Original languageEnglish (US)
Title of host publicationFormal Methods and Software Engineering - 21st International Conference on Formal Engineering Methods, ICFEM 2019, Proceedings
EditorsYamine Ait-Ameur, Shengchao Qin
PublisherSpringer
Pages336-352
Number of pages17
ISBN (Print)9783030324087
DOIs
StatePublished - 2019
Event21st International Conference on Formal Engineering Methods, ICFEM 2019 - Shenzhen, China
Duration: Nov 5 2019Nov 9 2019

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume11852 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference21st International Conference on Formal Engineering Methods, ICFEM 2019
CountryChina
CityShenzhen
Period11/5/1911/9/19

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Solution Enumeration Abstraction: A Modeling Idiom to Enhance a Lightweight Formal Method'. Together they form a unique fingerprint.

Cite this