AlloyMax: bringing maximum satisfaction to relational specifications
Abstract
Alloy is a declarative modeling language based on a first-order relational logic. Its constraint-based analysis has enabled a wide range of applications in software engineering, including configuration synthesis, bug finding, test-case generation, and security analysis. Certain types of analysis tasks in these domains involve finding an optimal solution. For example, in a network configuration problem, instead of finding any valid configuration, it may be desirable to find one that is most permissive (i.e., it permits a maximum number of packets). Due to its dependence on SAT, however, Alloy cannot be used to specify and analyze these types of problems.
BibTeX
@inproceedings{Zhang-al:FSE21,
author = {Changjian Zhang and
Ryan Wagner and
Pedro Orvalho and
David Garlan and
Vasco Manquinho and
Ruben Martins and
Eunsuk Kang},
title = {{AlloyMax:} bringing maximum satisfaction to relational specifications},
booktitle = {{ESEC/SIGSOFT} {FSE}},
pages = {155--167},
publisher = {{ACM}},
year = {2021},
}