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

DOI10.1007/S10703-016-0267-2MaRDI QIDQ2009609zbMATH OpenOpenAlexFDO

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

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

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• A confluent relational calculus for higher-order programming with constraints
• An algebraic perspective of constraint logic programming
• Relational constraint solving in SMT
• A synthesis of constraint satisfaction and constraint solving
• Constraint satisfaction with succinctly specified relations
• Verification, Model Checking, and Abstract Interpretation
• Universal algebraic methods for constraint satisfaction problems

Cites work

• scientific article; zbMATH DE number 3168330 (Why is no real title available?)
• scientific article; zbMATH DE number 1956604 (Why is no real title available?)
• scientific article; zbMATH DE number 1542661 (Why is no real title available?)
• Alloy*: a general-purpose higher-order relational constraint solver
• Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
• Dafny: an automatic program verifier for functional correctness
• Efficient E-Matching for SMT Solvers
• Isabelle/HOL. A proof assistant for higher-order logic
• Kodkod: A Relational Model Finder
• Model finding for recursive functions in SMT
• Nitpick: a counterexample generator for higher-order logic based on a relational model finder

Cited in

(6)

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

Describes a project that uses

Uses Software

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

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2009609)