On Uniformly Sampling Traces of a Transition System (Extended Version)

TL;DR

This paper introduces TraceSampler, an algorithm that uses Algebraic Decision Diagrams to uniformly sample traces of a transition system with formal guarantees, improving coverage in constrained random verification.

Contribution

It presents the first algorithm with provable uniformity guarantees for sampling traces in transition systems, implemented in the TraceSampler tool.

Findings

TraceSampler outperforms existing methods in uniformity and efficiency

Provides formal guarantees on the distribution of sampled traces

Demonstrates effectiveness through extensive experiments

Abstract

A key problem in constrained random verification (CRV) concerns generation of input stimuli that result in good coverage of the system's runs in targeted corners of its behavior space. Existing CRV solutions however provide no formal guarantees on the distribution of the system's runs. In this paper, we take a first step towards solving this problem. We present an algorithm based on Algebraic Decision Diagrams for sampling bounded traces (i.e. sequences of states) of a sequential circuit with provable uniformity (or bias) guarantees, while satisfying given constraints. We have implemented our algorithm in a tool called TraceSampler. Extensive experiments show that TraceSampler outperforms alternative approaches that provide similar uniformity guarantees.