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

DOI10.1007/S10703-016-0267-2zbMATH Open1425.68264OpenAlexW2582748022MaRDI QIDQ2009609FDOQ2009609

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

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

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)

Cites Work

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

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

Uses Software

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

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)