Skip to main content

Demur: checking functional-program properties using bounded recursion

Thompson, Simon, Runciman, Colin (2015) Demur: checking functional-program properties using bounded recursion. In: Sixth Workshop on Tools for Automatic Program Analysis, 08 Sep 2015, Saint-Malo, France. (Access to this publication is currently restricted. You may be able to access a copy if URLs are provided)

PDF - Publisher pdf
Restricted to Repository staff only
Contact us about this Publication Download (102kB)


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.

Item Type: Conference or workshop item (Lecture)
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming, > QA76.76 Computer software
Divisions: Faculties > Sciences > School of Computing > Programming Languages and Systems Group
Depositing User: Simon Thompson
Date Deposited: 15 Sep 2015 17:13 UTC
Last Modified: 29 May 2019 16:00 UTC
Resource URI: (The current URI for this page, for reference purposes)
  • Depositors only (login required):


Downloads per month over past year