Skip to main content
Kent Academic Repository

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) (KAR id:50496)

PDF Publisher pdf
Language: English

Restricted to Repository staff only
[thumbnail of TAPAS_2015_submission_1.pdf]


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: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: S. Thompson
Date Deposited: 15 Sep 2015 17:13 UTC
Last Modified: 17 Aug 2022 10:59 UTC
Resource URI: (The current URI for this page, for reference purposes)

University of Kent Author Information

  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.