Portus: Linking Alloy with SMT-based Finite Model Finding

TL;DR

Portus presents an SMT-based finite model finding backend for Alloy by translating models into $MSFOL$ and solving with Fortress, grounding the problem in the decidable $EUF$ fragment and integrating it with the Alloy Analyzer. The approach combines a general translation, novel sort resolution, and multiple optimizations to leverage SMT solvers, achieving competitive performance with Kodkod on expert benchmarks and showing better scaling on some features. Key contributions include handling many Alloy constructs (signatures, fields, non-exact scopes, and cardinality) through a multi-sort translation, scalar recognition, and constants-based scope axioms, plus extensive evaluation across correctness, performance, and scalability. The work enables a solver portfolio approach for Alloy, enabling hybrid analysis over bounded and unbounded scopes with practical implications for scalable formal modeling and verification tasks.

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 64 Alloy models written by experts. Our method is fully integrated into the Alloy Analyzer.

Figures (15)

• Figure 1: Definition of $\mathsf{resolvant}$: Alloy_ expression $\longrightarrow$ set(sort_expression).
• Figure 2: Alloy signatures example.
• Figure 3: Examples of Alloy fields.
• Figure 4: Translation of logical operators.
• Figure 5: Translation of set operators.