Datatypes with shared selectors

DOI10.1007/978-3-319-94205-6_39MaRDI QIDQ1799121zbMATH OpenOpenAlexFDO

Authors Andrew Reynolds, Arjun Viswanathan, Haniel Barbosa, Cesare Tinelli, Clark Barrett

Publication date 18 October 2018

Full work available at URL https://doi.org/10.1007/978-3-319-94205-6_39

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65)

Recommendations

• A decision procedure for (co)datatypes in SMT solvers
• A decision procedure for (co)datatypes in SMT solvers
• Counterexample-guided quantifier instantiation for synthesis in SMT
• Combined Satisfiability Modulo Parametric Theories
• Refutation-based synthesis in SMT

Cited in

(6)

• Synthesising programs with non-trivial constants
• Syntax-guided quantifier instantiation
• Unified selection from lists, arrays, and objects.
• Politeness for the theory of algebraic datatypes
• Superposition with datatypes and codatatypes
• Polite combination of algebraic datatypes

Describes a project that uses

Uses Software

• Dafny
• Isabelle/HOL
• SMT-LIB
• z3
• Sledgehammer
• StarExec
• Leon
• CVC4

This page was built for publication: Datatypes with shared selectors

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