Alloy*
Alloy*: a general-purpose higher-order relational constraint solver. The last decade has seen a dramatic growth in the use of constraint solvers as a computational mechanism, not only for analysis of software, but also at runtime. Solvers are available for a variety of logics but are generally restricted to first-order formulas. Some tasks, however, most notably those involving synthesis, are inherently higher order; these are typically handled by embedding a first-order solver (such as a SAT or SMT solver) in a domain-specific algorithm. Using strategies similar to those used in such algorithms, we show how to extend a first-order solver (in this case Kodkod, a model finder for relational logic used as the engine of the Alloy Analyzer) so that it can handle quantifications over higher-order structures. The resulting solver is sufficiently general that it can be applied to a range of problems; it is higher order, so that it can be applied directly, without embedding in another algorithm; and it performs well enough to be competitive with specialized tools. Just as the identification of first-order solvers as reusable backends advanced the performance of specialized tools and simplified their architecture, factoring out higher-order solvers may bring similar benefits to a new class of tools.
Keywords for this software
References in zbMATH (referenced in 6 articles )
Showing results 1 to 6 of 6.
Sorted by year (- Schneider, Sven; Lambers, Leen: Evaluation diversity for graph conditions (2021)
- Correia, Alexandre; Iyoda, Juliano; Mota, Alexandre: Combining model finder and genetic programming into a general purpose automatic program synthesizer (2020)
- Milicevic, Aleksandar; Near, Joseph P.; Kang, Eunsuk; Jackson, Daniel: Alloy*: a general-purpose higher-order relational constraint solver (2019)
- Porncharoenwase, Sorawee; Nelson, Tim; Krishnamurthi, Shriram: CompoSAT: specification-guided coverage for model finding (2018)
- Zulkoski, Edward; Bright, Curtis; Heinle, Albert; Kotsireas, Ilias; Czarnecki, Krzysztof; Ganesh, Vijay: Combining SAT solvers with computer algebra systems to verify combinatorial conjectures (2017)
- Mota, Alexandre; Iyoda, Juliano; Maranhão, Heitor: Program synthesis by model finding (2016) ioport