Journal article
Dynamite
Abstract
Automatic analysis of Alloy models is supported by the Alloy Analyzer, a tool that translates an Alloy model to a propositional formula that is then analyzed using off-the-shelf SAT solvers. The translation requires user-provided bounds on the sizes of data domains. The analysis is limited by the bounds and is therefore partial. Thus, the Alloy Analyzer may not be appropriate for the analysis of critical applications where more conclusive …
Authors
Moscato MM; Pombo CGL; Frias MF
Journal
ACM Transactions on Software Engineering and Methodology, Vol. 23, No. 2, pp. 1–37
Publisher
Association for Computing Machinery (ACM)
Publication Date
3 2014
DOI
10.1145/2544136
ISSN
1049-331X