Analyzing Alloy Formulas using an SMT Solver: A Case Study

TL;DR

This paper demonstrates how Yices SMT solver can analyze Alloy models beyond finitized types, enabling more general reasoning and potentially proving tautologies, with experimental comparison to Alloy Analyzer.

Contribution

It introduces a novel approach using Yices for Alloy analysis that overcomes type finitization limitations and can prove tautologies.

Findings

Yices analysis can handle more general Alloy models.

The approach can prove assertions as tautologies.

Experimental results show performance differences with Alloy Analyzer.

Abstract

This paper describes how Yices, a modern SAT Modulo theories solver, can be used to analyze the address-book problem expressed in Alloy, a first-order relational logic with transitive closure. Current analysis of Alloy models - as performed by the Alloy Analyzer - is based on SAT solving and thus, is done only with respect to finitized types. Our analysis generalizes this approach by taking advantage of the background theories available in Yices, and avoiding type finitization when possible. Consequently, it is potentially capable of proving that an assertion is a tautology - a capability completely missing from the Alloy Analyzer. This paper also reports on our experimental results that compare the performance of our analysis to that of the Alloy Analyzer for various versions of the address book problem.