-
Portus: Linking Alloy with SMT-based Finite Model Finding
Authors:
Ryan Dancy,
Nancy A. Day,
Owen Zila,
Khadija Tariq,
Joseph Poremba
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…
▽ More
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.
△ Less
Submitted 23 May, 2025; v1 submitted 24 November, 2024;
originally announced November 2024.
-
Diversity in Software Engineering Conferences and Journals
Authors:
Aditya Shankar Narayanan,
Dheeraj Vagavolu,
Nancy A Day,
Meiyappan Nagappan
Abstract:
Diversity with respect to ethnicity and gender has been studied in open-source and industrial settings for software development. Publication avenues such as academic conferences and journals contribute to the growing technology industry. However, there have been very few diversity-related studies conducted in the context of academia. In this paper, we study the ethnic, gender, and geographical div…
▽ More
Diversity with respect to ethnicity and gender has been studied in open-source and industrial settings for software development. Publication avenues such as academic conferences and journals contribute to the growing technology industry. However, there have been very few diversity-related studies conducted in the context of academia. In this paper, we study the ethnic, gender, and geographical diversity of the authors published in Software Engineering conferences and journals. We provide a systematic quantitative analysis of the diversity of publications and organizing and program committees of three top conferences and two top journals in Software Engineering, which indicates the existence of bias and entry barriers towards authors and committee members belonging to certain ethnicities, gender, and/or geographical locations in Software Engineering conferences and journal publications. For our study, we analyse publication (accepted authors) and committee data (Program and Organizing committee/ Journal Editorial Board) from the conferences ICSE, FSE, and ASE and the journals IEEE TSE and ACM TOSEM from 2010 to 2022. The analysis of the data shows that across participants and committee members, there are some communities that are consistently significantly lower in representation, for example, publications from countries in Africa, South America, and Oceania. However, a correlation study between the diversity of the committees and the participants did not yield any conclusive evidence. Furthermore, there is no conclusive evidence that papers with White authors or male authors were more likely to be cited. Finally, we see an improvement in the ethnic diversity of the authors over the years 2010-2022 but not in gender or geographical diversity.
△ Less
Submitted 24 October, 2023;
originally announced October 2023.
-
Astra Version 1.0: Evaluating Translations from Alloy to SMT-LIB
Authors:
Ali Abbassi,
Nancy A. Day,
Derek Rayside
Abstract:
We present a variety of translation options for converting Alloy to SMT-LIB via Alloy's Kodkod interface. Our translations, which are implemented in a library that we call Astra, are based on converting the set and relational operations of Alloy into their equivalent in typed first-order logic (TFOL). We investigate and compare the performance of an SMT solver for many translation options. We comp…
▽ More
We present a variety of translation options for converting Alloy to SMT-LIB via Alloy's Kodkod interface. Our translations, which are implemented in a library that we call Astra, are based on converting the set and relational operations of Alloy into their equivalent in typed first-order logic (TFOL). We investigate and compare the performance of an SMT solver for many translation options. We compare using only one universal type to recovering Alloy type information from the Kodkod representation and using multiple types in TFOL. We compare a direct translation of the relations to predicates in TFOL to one where we recover functions from their relational form in Kodkod and represent these as functions in TFOL. We compare representations in TFOL with unbounded scopes to ones with bounded scopes, either pre or post quantifier expansion. Our results across all these dimensions provide directions for portfolio solvers, modelling improvements, and optimizing SMT solvers.
△ Less
Submitted 13 June, 2019;
originally announced June 2019.
-
Which Classes of Structures Are Both Pseudo-elementary and Definable by an Infinitary Sentence?
Authors:
Will Boney,
Barbara F. Csima,
Nancy A. Day,
Matthew Harrison-Trainor
Abstract:
When classes of structures are not first-order definable, we might still try to find a nice description. There are two common ways for doing this. One is to expand the language, leading to notions of pseudo-elementary classes, and the other is to allow infinite conjuncts and disjuncts. In this paper we examine the intersection. Namely, we address the question: Which classes of structures are both…
▽ More
When classes of structures are not first-order definable, we might still try to find a nice description. There are two common ways for doing this. One is to expand the language, leading to notions of pseudo-elementary classes, and the other is to allow infinite conjuncts and disjuncts. In this paper we examine the intersection. Namely, we address the question: Which classes of structures are both pseudo-elementary and $\mathcal{L}_{ω_1 ω}$-elementary? We find that these are exactly the classes that can be defined by an infinitary formula that has no infinitary disjunctions.
△ Less
Submitted 30 April, 2020; v1 submitted 5 August, 2018;
originally announced August 2018.
