You are viewing a javascript disabled version of the site. Please enable Javascript for this site to function properly.
Go to headerGo to navigationGo to searchGo to contentsGo to footer
In content section. Select this link to jump to navigation

An Abstract Decision Procedure for a Theory of Inductive Data Types


Inductive data types are a valuable modeling tool for software verification. In the past, decision procedures have been proposed for various theories of inductive data types, some focused on the universal fragment, and some focused on handling arbitrary quantifiers. Because of the complexity of the full theory, previous work on the full theory has not focused on strategies for practical implementation. However, even for the universal fragment, previous work has been limited in several significant ways. In this paper, we present a general and practical algorithm for the universal fragment. The algorithm is presented declaratively as a set of abstract rules which we show to be terminating, sound, and complete. We show how other algorithms can be realized as strategies within our general framework, and we propose a new strategy and give experimental results indicating that it performs well in practice. We conclude with a discussion of several useful ways the algorithm can be extended.