Cesare Tinelli's Publications
Clark Barrett, Igor Shikanian and Cesare Tinelli. An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types. In Proceedings of the of the 4th International Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR'06), 2006.
Abstract. The theory of recursive data types is a valuable modeling tool for software verifica- tion. 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 is significantly faster than other strategies.