TY - JOUR
T1 - An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types
AU - Barrett, Clark
AU - Shikanian, Igor
AU - Tinelli, Cesare
N1 - Funding Information:
We are grateful to the anonymous referee for valuable comments that helped to improve the present Letter. The numerical simulations reported here were carried out on Fujitsu-made vector parallel processors (VPP5000) kindly made available by the Astronomical Data Analysis Center (ADAC) at the National Astronomical Observatory of Japan (NAOJ) for our research project why36b. K. B. and D. A. F. acknowledge the financial support of the Australian Research Council throughout the course of this work. H. Y. acknowledges the support of the research fellowships of the Japan Society for the Promotion of Science for Young Scientists (17-10511).
PY - 2007/6/20
Y1 - 2007/6/20
N2 - 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.
AB - 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.
KW - decision procedures
KW - recursive data types
KW - satisfiability modulo theories
KW - term algebras
UR - http://www.scopus.com/inward/record.url?scp=34249903869&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=34249903869&partnerID=8YFLogxK
U2 - 10.1016/j.entcs.2006.11.037
DO - 10.1016/j.entcs.2006.11.037
M3 - Article
AN - SCOPUS:34249903869
VL - 174
SP - 23
EP - 37
JO - Electronic Notes in Theoretical Computer Science
JF - Electronic Notes in Theoretical Computer Science
SN - 1571-0661
IS - 8
ER -