Cesare Tinelli's Publications

Clark Barrett, Igor Shikanian and Cesare Tinelli. An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types. Journal on Satisfiability, Boolean Modeling and Computation, 3:1-17, 2007.

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 declara- tively 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 showing that it performs well in practice. We conclude with a discussion of several useful ways the algorithm can be extended.