An Abstract Decision Procedure for Algebraic Data Types

Опубликовано 7 сентября 2016, 16:38

The theory of algebraic 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. I will 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. I will show how other algorithms can be realized as strategies within our general framework, and I will propose a new strategy and give experimental results showing that it is significantly better than other strategies.