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

PDF Publisher pdf
Language: English

Restricted to Repository staff only
Contact us about this Publication
[thumbnail of TAPAS_2015_submission_1.pdf]

Abstract

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: Simon Thompson
Date Deposited: 15 Sep 2015 17:13 UTC
Last Modified: 16 Feb 2021 13:28 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/50496 (The current URI for this page, for reference purposes)
Thompson, Simon: https://orcid.org/0000-0002-2350-301X
  • Depositors only (login required):

Downloads

Downloads per month over past year