An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types

Clark Barrett; Igor Shikanian; Cesare Tinelli

doi:10.1016/j.entcs.2006.11.037

Back

An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types

Journal article

Open access

An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types

Clark Barrett, Igor Shikanian and Cesare Tinelli

Electronic notes in theoretical computer science, Vol.174(8), pp.23-37

06/20/2007

DOI: 10.1016/j.entcs.2006.11.037

Files and links (1)

url

https://doi.org/10.1016/j.entcs.2006.11.037View

Published (Version of record) Open Access

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.

decision procedures

recursive data types

satisfiability modulo theories

term algebras

Details

Title: Subtitle: An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types
Creators: Clark Barrett - New York University
Igor Shikanian - New York University
Cesare Tinelli - University of Iowa
Resource Type: Journal article
Publication Details: Electronic notes in theoretical computer science, Vol.174(8), pp.23-37
DOI: 10.1016/j.entcs.2006.11.037
ISSN: 1571-0661
eISSN: 1571-0661
Publisher: Elsevier B.V
Language: English
Date published: 06/20/2007
Academic Unit: Computer Science
Record Identifier: 9984259406302771

Metrics

19 Record Views

13 Times Cited - Web of Science