AlloyMax: bringing maximum satisfaction to relational specifications
Changjian Zhang, Ryan Wagner, Pedro Orvalho, David Garlan, Vasco M. Manquinho, Ruben Martins, Eunsuk Kang · 2021
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.