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

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

Daniel Jackson, Aleksandar Milicevic, Eunsuk Kang, 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

synthesisdesignhigher-order logicmodel findingAlloy

Mathematics Subject Classification ID

Related Items (5)

Combining SAT solvers with computer algebra systems to verify combinatorial conjectures ⋮ Special issue on syntax-guided synthesis preface ⋮ Alloy*: a general-purpose higher-order relational constraint solver ⋮ Combining model finder and genetic programming into a general purpose automatic program synthesizer ⋮ CompoSAT: specification-guided coverage for model finding

Uses Software

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Isabelle/HOL. A proof assistant for higher-order logic
• Alloy*: a general-purpose higher-order relational constraint solver
• Model Finding for Recursive Functions in SMT
• Dafny: An Automatic Program Verifier for Functional Correctness
• Efficient E-Matching for SMT Solvers
• Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
• Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder
• Kodkod: A Relational Model Finder

This page was built for publication: Alloy*: a general-purpose higher-order relational constraint solver