Abstract
The theory of recursive data types is a valuable modeling tool for software verification. In the past, decision procedures have been proposed for both the full theory and its universal fragment. However, previous work has been limited in various ways. In this paper, we present a general algorithm for the universal fragment. The algorithm is presented declaratively as a set of abstract rules which are terminating, sound, and complete. We show how other algorithms can be realized as strategies within our general framework. Finally, we propose a new strategy and give experimental results showing that it performs well in practice.
| Original language | English (US) |
|---|---|
| Pages (from-to) | 23-37 |
| Number of pages | 15 |
| Journal | Electronic Notes in Theoretical Computer Science |
| Volume | 174 |
| Issue number | 8 |
| DOIs | |
| State | Published - Jun 20 2007 |
Keywords
- decision procedures
- recursive data types
- satisfiability modulo theories
- term algebras
ASJC Scopus subject areas
- Theoretical Computer Science
- Computer Science(all)
Fingerprint Dive into the research topics of 'An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types'. Together they form a unique fingerprint.
Cite this
Barrett, C., Shikanian, I., & Tinelli, C. (2007). An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types. Electronic Notes in Theoretical Computer Science, 174(8), 23-37. https://doi.org/10.1016/j.entcs.2006.11.037