Portus: Linking Alloy with SMT-based Finite Model Finding

Alloy is a well-known, formal, declarative language for modelling systems early in the software development process. Currently, it uses the Kodkodlibrary as a back-end for finite model finding. Kodkodtranslates 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 Fortresslibrary, creating an alternative back-end for the AlloyAnalyzer. Fortressconverts 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 Portuswith Kodkodon a corpus of 63 Alloy models written by experts. Our method is fully integrated into the AlloyAnalyzer.