Research on Alloy specification language presented at top software engineering conference

A team of INESC TEC researchers working on the Alloy language and specification tool presented the QAlloy extension at the ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE), a top conference in the area of software engineering that took place between November 14 and 18, in Singapore.

Although Alloy is a very popular formal method in software design, it is not suitable to quantitative problems, i.e., data mining, machine learning, quantum computing, real-time systems, etc. The paper “Quantitative relational modelling with QAlloy” presents an extension, called QAlloy, to address this type of problems, thus tackling these limitations.

“The QAlloy solution, which extends the Alloy standard, a tool developed at the Massachusetts Institute of Technology (MIT) and made publicly available, is capable of analysing quantitative models without impairing the simplicity of language and its use in practical problems”, said Pedro Silva, one of the authors of the paper. In this sense, “this solution provides a modelling and analysis tool that deals, in a simple and effective way, with quantification-related problems”, added the researcher.

This tool can be applied to problems already supported by the Alloy language, but also to problems that present critical properties of a quantitative nature in the integers’ domain. Other solutions to support different quantitative domains, e.g., probabilistic to allow modelling problems with uncertainty, are currently being explored.


This paper was written by researchers at INESC TEC’s High-Assurance Software Laboratory (HASLab), Alcino Cunha and José Nuno Oliveira, also teachers at the School of Engineering of the University of Minho, Nuno Macedo, teacher at the Faculty of Engineering of the University of Porto, and Pedro Silva.

ESEC/FSE is a top conference in fundamentals of software engineering, classified as A*, according to the Australian core ranking that provides assessments of major conferences in the areas of computing.

The INESC TEC researchers mentioned in this news piece are associated with INESC TEC, UMinho and UP-FEUP.

Photo credits: ESEC/FSE 2022