Automatic Synthesis of Random Generators for Numerically Constrained Algebraic Recursive Types

TL;DR

This paper introduces Testify, a framework that automatically synthesizes uniform random generators for constrained recursive data structures, enhancing program verification through constraint-based random testing.

Contribution

It presents a novel method to automatically generate uniform random test data for complex, constrained recursive data structures in program verification.

Findings

Successfully synthesizes uniform random generators for various data structures.

Ensures generated test cases satisfy high-level constraints and properties.

Demonstrates practical effectiveness through multiple use-cases and experiments.

Abstract

In program verification, constraint-based random testing is a powerful technique which aims at generating random test cases that satisfy functional properties of a program. However, on recursive constrained data-structures (e.g., sorted lists, binary search trees, quadtrees), and, more generally, when the structures are highly constrained, generating uniformly distributed inputs is difficult. In this paper, we present Testify: a framework in which users can define algebraic data-types decorated with high-level constraints. These constraints are interpreted as membership predicates that restrict the set of inhabitants of the type. From these definitions, Testify automatically synthesises a partial specification of the program so that no function produces a value that violates the constraints (e.g. a binary search tree where nodes are improperly inserted). Our framework augments the original program with tests that check such properties. To achieve that, we automatically produce uniform random samplers that generate values which satisfy the constraints, and verifies the validity of the outputs of the tested functions. By generating the shape of a recursive data-structure using Boltzmann sampling and generating evenly distributed finite domain variable values using constraint solving, our framework guarantees size-constrained uniform sampling of test cases. We provide use-cases of our framework on several key data structures that are of practical relevance for developers. Experiments show encouraging results.