Demur: checking functional-program properties using bounded recursion

The Demur tool translates programs and properties expressed in a large subset of Haskell to decidable models in Z3. These models use a bounded-depth representation of recursive function definitions, where the bound is increased from zero as checking proceeds. An explicit and distinguishable representation of undefined parts of data values enables Demur to maximize property-checking power despite approximation – for example, by using parallel three-valued logical operators. Several case-studies present a mixture of successes and failures in comparison with current widely-used tools for property checking. Possible routes to improved performance are identified. Comparisons are drawn with other Z3-based tools with functional-language translators, such as Leon and Halo.