@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",
year = "2017",
month = jan,
day = "1",
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",
note = "6th Workshop on Software Quality Analysis, Monitoring, Improvement, and Applications, SQAMIA 2017 ; Conference date: 11-09-2017 Through 13-09-2017",
}