Alloy*: a general-purpose higher-order relational constraint solver

DOI10.1007/s10703-016-0267-2zbMath1425.68264MaRDI QIDQ2009609

Daniel Jackson, Eunsuk Kang, Aleksandar Milicevic, Joseph P. Near

Publication date: 29 November 2019

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://hdl.handle.net/1721.1/135729

zbMATH Keywords

synthesis; design; higher-order logic; model finding; Alloy

Mathematics Subject Classification ID

68Q60: Specification and verification (program logics, model checking, etc.)

68T20: Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)

Uses Software

• Dafny
• Nitpick
• Isabelle/HOL
• z3
• Kodkod
• TestEra
• TACO
• Boogie
• HMC
• Alloy*
• GitHub
• Rosette
• margrave
• Nunchaku