An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types
From MaRDI portal
Publication:2864522
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
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
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