Portus: Linking Alloy with SMT-based Finite Model Finding

TL;DR

Portus introduces an SMT-based back-end for Alloy, translating models into MSFOL and EUF to handle larger and more complex problems than traditional SAT-based methods.

Contribution

It presents a novel translation from Alloy to MSFOL and integrates SMT solving as an alternative back-end for Alloy analysis.

Findings

Portus outperforms Kodkod on larger models.

The method supports more complex and larger models.

Integration into Alloy Analyzer is seamless.

Abstract

Alloy is a well-known, formal, declarative language for modelling systems early in the software development process. Currently, it uses the Kodkod library as a back-end for finite model finding. Kodkod translates the model to a SAT problem; however, this method can often handle only problems of fairly low-size sets and is inherently finite. We present Portus, a method for translating Alloy into an equivalent many-sorted first-order logic problem (MSFOL). Once in MSFOL, the problem can be evaluated by an SMT-based finite model finding method implemented in the Fortress library, creating an alternative back-end for the Alloy Analyzer. Fortress converts the MSFOL finite model finding problem into the logic of uninterpreted functions with equality (EUF), a decidable fragment of first-order logic that is well-supported in many SMT solvers. We compare the performance of Portus with Kodkod on a corpus of 63 Alloy models written by experts. Our method is fully integrated into the Alloy Analyzer.