@inproceedings{47d05c2f9a684dda974fbb6087473137,
title = "Evaluating state modeling techniques in alloy",
abstract = "Software models help develop higher quality systems. The declarative language Alloy and its accompanying automatic analyzer embody a method for developing software models. Our focus in this paper is Alloy models of systems where different operations may mutate the system state, e.g., addition of an element to a sorted container. Researchers have previously used two techniques for modeling state and state mutation in Alloy, but these techniques have not been compared to each other. We propose a third technique and evaluate all these three techniques that embody conceptually different modeling approaches. We use four core subjects, which we model using each technique. Our primary goal is to quantitatively evaluate the techniques by considering the runtime for solving the ensuing SAT formulas. We also discuss practical tradeoffs among the techniques.",
keywords = "Alloy, Empirical evaluation, Predicate parameterization, SAT solving, State modeling",
author = "Allison Sullivan and Kaiyuan Wang and Sarfraz Khurshid and Darko Marinov",
note = "Funding Information: This research was partially supported by the NSF Grant Nos. CNS-1239498, CCF-1319688, CCF-1409423, and CCF-1421503. Authors{\textquoteright} addresses: Allison Sullivan, Kaiyuan Wang, and Sarfraz Khurshid, Department of Electrical and Computer Engineering, The University of Texas at Austin, Austin, TX 78712, USA; Darko Marinov, Department of Computer Science, University of Illinois at Urbana-Champaign, Urbana, IL 61801, USA. Email correspondence: khurshid@utexas.edu Copyright {\textcopyright}by the paper{\textquoteright}s authors. Copying permitted only for private and academic purposes. In: Z. Budimac (ed.): Proceedings of the SQAMIA 2017: 6th Workshop on Software Quality, Analysis, Monitoring, Improvement, and Applications, Belgrade, Serbia, 11-13.9.2017, Also published online by CEUR Workshop Proceedings (http://ceur-ws.org, ISSN 1613-0073) Publisher Copyright: {\textcopyright} Copyright 2017 by the paper's authors.; 6th Workshop on Software Quality Analysis, Monitoring, Improvement, and Applications, SQAMIA 2017 ; Conference date: 11-09-2017 Through 13-09-2017",
year = "2017",
language = "English (US)",
series = "CEUR Workshop Proceedings",
publisher = "CEUR-WS",
editor = "Zoran Budimac",
booktitle = "SQAMIA 2017 - Proceedings of the 6th Workshop on Software Quality Analysis, Monitoring, Improvement, and Applications",
}