Portus: Linking Alloy with SMT-based Finite Model Finding
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.
Cite
@article{arxiv.2411.15978,
title = {Portus: Linking Alloy with SMT-based Finite Model Finding},
author = {Ryan Dancy and Nancy A. Day and Owen Zila and Khadija Tariq and Joseph Poremba},
journal= {arXiv preprint arXiv:2411.15978},
year = {2026}
}