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

(7)

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

Describes a project that uses

Uses Software

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

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)