An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types

DOI10.1016/j.entcs.2006.11.037zbMath1277.68132MaRDI QIDQ2864522

Cesare Tinelli, Clark Barrett, Igor Shikanian

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

recursive data types; satisfiability modulo theories; decision procedures; term algebras

Mathematics Subject Classification ID

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

Related Items

Locality Results for Certain Extensions of Theories with Bridging Functions, Reasoning about algebraic data types with abstractions, Syntax-guided quantifier instantiation, Efficiently solving quantified bit-vector formulas, An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types, Rewrite-Based Satisfiability Procedures for Recursive Data Structures

Uses Software

• CVC Lite

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Abstract congruence closure
• An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types
• Fast Decision Procedures Based on Congruence Closure
• Simplification by Cooperating Decision Procedures
• Reasoning About Recursively Defined Data Structures
• An Efficient Unification Algorithm
• Automated Reasoning
• Computer Aided Verification
• Splitting on Demand in SAT Modulo Theories
• Logics in Artificial Intelligence
• Theorem Proving in Higher Order Logics