Logo image
Back
An Abstract Decision Procedure for a Theory of Inductive Data Types
Journal article   Open access   Peer reviewed

An Abstract Decision Procedure for a Theory of Inductive Data Types

Clark Barrett, Igor Shikanian and Cesare Tinelli
Journal on satisfiability, Boolean modeling and computation, Vol.3(1-2), pp.21-46
07/01/2007
DOI: 10.3233/SAT190028
url
https://doi.org/10.3233/SAT190028View
Published (Version of record) Open Access

Abstract

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.

Details

Metrics

15 Record Views
Logo image