CMU Researchers Tapped for ACM Distinguished Paper Award

A joint team of researchers from Carnegie Mellon University and the University of Lisbon will receive an ACM SIGSOFT Distinguished Paper Award at the upcoming ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE 2021) for their work on a new analysis engine for the popular Alloy modeling language.

The conference is an internationally renowned forum for researchers, practitioners, and educators to present and discuss the most recent innovations, trends, experiences, and challenges in the field of software engineering. Distinguished papers are given to at most 10% of the papers accepted at an ACM SIGSOFT-sponsored conference. 

Changjian (CJ) Zhang, a software engineering Ph.D. student in the Institute for Software Research (ISR), was the lead author on “AlloyMax: Bringing Maximum Satisfaction to Relational Specifications” which extends the popular declarative modeling language Alloy with new, significant capabilities. While the language has enabled numerous applications in software engineering, Alloy is not designed for finding an optimal solution, which limits the range of problems that it can be used to solve.For example, it cannot be used to find a network configuration solution that permits the maximum number of packets to be transmitted.

To address this, the team introduced not only additional Alloy language constructs to account for problems involving optimality but also created a new analysis engine that leverages a Maximum Satisfiability (MaxSAT) solver to generate optimal solutions.

“Getting the design right is critical for software, especially in systems like medical devices and web applications, where a design defect can lead to safety or security failures,” said Eunsuk Kang, assistant professor in ISR and a co-author on the paper “Alloy is already an important part of catching these potentially catastrophic defects before a single line of code is written,” Kang points out. “Our work on AlloyMax extends Alloy in a way that makes it more powerful, by extending the range of analysis problems that it can tackle. In particular, the extension allows Alloy to be used for optimization problems, where the goal is to find an optimal design solution that maximizes certain types of quality attributes, such as performance and safety.”

The team was grateful and humbled by the recognition. 

“It is a great honor to get recognized for the collective effort of our collaborators at CMU and the CMU-Portugal program,” Zhang and Kang said. “We hope that increased visibility of this work means more people will find out about our tool and benefit from using it.”

Paper Reference: AlloyMax: Bringing Maximum Satisfaction to Relational Specifications 

Team members: Changjian Zhang (CMU), Ryan Wagner (CMU), Pedro Orvalho (INESC-ID/IST, Universidade de Lisboa), David Garlan (CMU), Vasco Manquinho (INESC-ID/IST, Universidade de Lisboa), Ruben Martins (CMU), and Eunsuk Kang (CMU).