Solver-based sketching of alloy models using test valuations

Kaiyuan Wang, Allison Sullivan, Darko Marinov, Sarfraz Khurshid

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

Abstract

We introduce ASketch, the first framework for sketching models in the Alloy language. The Alloy Analyzer is a SAT-based constraint solver that allows users to create valuations for relations with respect to given constraints and bound on the universe of discourse. Alloy users routinely use the valuations to validate their models: enumerate some valuations and inspect them to detect underconstraints or overconstraints. Our key insight is that valid and invalid valuations enable sketching Alloy models where the user writes a partial model with holes and provides some valuations, and the sketching infrastructure completes the model by synthesizing Alloy fragments for the holes. ASketch offers the following extensions to Alloy: (1) it expands the Alloy grammar, allowing users to write holes in an Alloy model; (2) it can parse regular expressions and automatically generate pools of matching fragments to replace the holes; (3) it includes a solver-based technique that encodes the model with holes, the fragments for each hole, and the expected valuations to a meta-model which completes the holes when solved. Experimental results show that ASketch works well for different Alloy models with various number of holes, providing a promising approach to bring the success of traditional program sketching for imperative and functional programs to declarative, relational logic.

Original languageEnglish (US)
Title of host publicationAbstract State Machines, Alloy, B, TLA, VDM, and Z - 6th International Conference, ABZ 2018, Proceedings
EditorsMichael Butler, Thai Son Hoang, Alexander Raschke, Klaus Reichl
PublisherSpringer-Verlag Berlin Heidelberg
Pages121-136
Number of pages16
ISBN (Print)9783319912707
DOIs
StatePublished - Jan 1 2018
Event6th International Conference on ABZ Conference on ASM, Alloy, B, TLA, VDM, and Z, ABZ 2018 - Southampton, United Kingdom
Duration: Jun 5 2018Jun 8 2018

Publication series

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

Other

Other6th International Conference on ABZ Conference on ASM, Alloy, B, TLA, VDM, and Z, ABZ 2018
CountryUnited Kingdom
CitySouthampton
Period6/5/186/8/18

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Solver-based sketching of alloy models using test valuations'. Together they form a unique fingerprint.

  • Cite this

    Wang, K., Sullivan, A., Marinov, D., & Khurshid, S. (2018). Solver-based sketching of alloy models using test valuations. In M. Butler, T. S. Hoang, A. Raschke, & K. Reichl (Eds.), Abstract State Machines, Alloy, B, TLA, VDM, and Z - 6th International Conference, ABZ 2018, Proceedings (pp. 121-136). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10817 LNCS). Springer-Verlag Berlin Heidelberg. https://doi.org/10.1007/978-3-319-91271-4_9