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

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

Clark Barrett, Igor Shikanian, Cesare Tinelli

Computer Science

Research output: Contribution to journal › Article › peer-review

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	https://doi.org/10.1016/j.entcs.2006.11.037
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)

Access to Document

10.1016/j.entcs.2006.11.037

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

@article{e1538e28fe30405a953a31c88d71925d,

title = "An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types",

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.",

keywords = "decision procedures, recursive data types, satisfiability modulo theories, term algebras",

author = "Clark Barrett and Igor Shikanian and Cesare Tinelli",

year = "2007",

month = jun,

day = "20",

doi = "10.1016/j.entcs.2006.11.037",

language = "English (US)",

volume = "174",

pages = "23--37",

journal = "Electronic Notes in Theoretical Computer Science",

issn = "1571-0661",

publisher = "Elsevier",

number = "8",

}

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

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 -

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

Abstract

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Cite this