An abstract decision procedure for satisfiability in the theory of recursive data types

DOI10.1016/J.ENTCS.2006.11.037MaRDI QIDQ2864522zbMATH OpenOpenAlexFDO

Authors Clark Barrett, Igor Shikanian, Cesare Tinelli

Publication date 6 December 2013

Published in Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.entcs.2006.11.037

zbMATH Keywords

satisfiability modulo theoriesdecision proceduresrecursive data typesterm algebras

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• An abstract decision procedure for a theory of inductive data types.
• Decision procedures for algebraic data types with abstractions
• A decision procedure for (co)datatypes in SMT solvers
• A decision procedure for (co)datatypes in SMT solvers
• Rewrite-based satisfiability procedures for recursive data structures
• scientific article; zbMATH DE number 88946
• Decidability properties of recursive types.
• A coinduction principle for recursive data types based on bisimulation
• Deterministic and nondeterministic computation, and horn programs, on abstract data types
• scientific article; zbMATH DE number 3936490

Cites work

• scientific article; zbMATH DE number 108434 (Why is no real title available?)
• scientific article; zbMATH DE number 1007358 (Why is no real title available?)
• A practical approach to partial functions in CVC Lite
• Abstract congruence closure
• An Efficient Unification Algorithm
• An abstract decision procedure for satisfiability in the theory of recursive data types
• Automated Reasoning
• Computer Aided Verification
• Fast Decision Procedures Based on Congruence Closure
• Logics in Artificial Intelligence
• Reasoning About Recursively Defined Data Structures
• Simplification by Cooperating Decision Procedures
• Splitting on Demand in SAT Modulo Theories
• Theorem Proving in Higher Order Logics

Cited in

(9)

• An abstract decision procedure for satisfiability in the theory of recursive data types
• Syntax-guided quantifier instantiation
• Efficiently solving quantified bit-vector formulas
• Reasoning about algebraic data types with abstractions
• Rewrite-based satisfiability procedures for recursive data structures
• Abstract GSOS rules and a modular treatment of recursive definitions
• Locality Results for Certain Extensions of Theories with Bridging Functions
• An abstract decision procedure for a theory of inductive data types.
• Decision procedures for algebraic data types with abstractions

Describes a project that uses

Uses Software

• CVC Lite

This page was built for publication: An abstract decision procedure for satisfiability in the theory of recursive data types

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