Fail Faster: Staging and Fast Randomness for High-Performance PBT

Proceedings of the ACM on Programming Languages · 2026-04-10

Property-based testing (PBT) relies on generators for random test cases, often constructed using embedded domain specific languages, which provide expressive combinators for building and composing generators. The effectiveness of PBT depends critically on the speed of these generators. However, careful measurements show that the generator performance of widely used PBT libraries falls well short of what is possible, due principally to (1) the abstraction overhead of their combinator-heavy style and (2) suboptimal sources of randomness. We characterize, quantify, and address these bottlenecks. To eliminate abstraction overheads, we propose a technique based on multi-stage programming, dubbed Allegro. We apply this technique to leading generator libraries in OCaml and Scala 3, significantly improving performance. To quantify the performance impact of the randomness source, we carry out a controlled experiment, replacing the randomness in the OCaml PBT library with an optimized version. Both interventions exactly preserve the semantics of generators, enabling precise, pointwise comparisons. Together, these improvements find bugs up to 13× faster.

Artifact for Fail Faster: Staging and Fast Randomness for High-Performance PBT

Zenodo (CERN European Organization for Nuclear Research) · 2026-02-24 · 1 citations

Hi! You've found the artifact for Fail Faster: Staging and Fast Randomness for High-Performance Property-Based Testing. Check out the GitHub project for further instructions.

Artifact: Code-Specify-Test-Debug-Prove: Flexibly Integrating Separation Logic Specification into Conventional Workflows

Zenodo (CERN European Organization for Nuclear Research) · 2026-04-17

This artifact (the Docker Image) contains the following components: our tools (CN, Fulminate, and Darcy), verification results for the pKVM hyp allocator, and an Android Linux with the instrumented hyp allocator. For the most up-to-date versions, refer to the following repositories: CN, Fulminate, and Darcy Cut-out hyp allocator with specifications and proofs Fulminate-Instrumented Android Linux NOTE: the authors of the repository given above are the authors of the paper "Code-Specify-Test-Debug-Prove: Flexibly Integrating Separation Logic Specification into Conventional Workflows", for which this repository contains additional materials. For information about authors and license of the source code, see the uploaded files. For instructions on how to use this artifact, please see README.md included in the artifact.

Artifact for Fail Faster: Staging and Fast Randomness for High-Performance PBT

Open MIND · 2026-02-24

Hi! You've found the artifact for Fail Faster: Staging and Fast Randomness for High-Performance Property-Based Testing. Check out the GitHub project for further instructions.

Code-Specify-Test-Debug-Prove: Flexibly Integrating Separation Logic Specification into Conventional Workflows

Zenodo (CERN European Organization for Nuclear Research) · 2026-03-18

This artifact (the Docker Image) contains the following components: our tools (CN, Fulminate, and Darcy), verification results for the pKVM hyp allocator, and an Android Linux with the instrumented hyp allocator. For the most up-to-date versions, refer to the following repositories: CN, Fulminate, and Darcy Cut-out hyp allocator with specifications and proofs Fulminate-Instrumented Android Linux NOTE: the authors of the repository given above are the authors of the paper "Code-Specify-Test-Debug-Prove: Flexibly Integrating Separation Logic Specification into Conventional Workflows", for which this repository contains additional materials. For information about authors and license of the source code, see the uploaded files. For instructions on how to use this artifact, please see README.md included in the artifact.

Code-Specify-Test-Debug-Prove: Flexibly Integrating Separation Logic Specification into Conventional Workflows

Zenodo (CERN European Organization for Nuclear Research) · 2026-03-18

This artifact (the Docker Image) contains the following components: our tools (CN, Fulminate, and Darcy), verification results for the pKVM hyp allocator, and an Android Linux with the instrumented hyp allocator. For the most up-to-date versions, refer to the following repositories: CN, Fulminate, and Darcy Cut-out hyp allocator with specifications and proofs Fulminate-Instrumented Android Linux NOTE: the authors of the repository given above are the authors of the paper "Code-Specify-Test-Debug-Prove: Flexibly Integrating Separation Logic Specification into Conventional Workflows", for which this repository contains additional materials. For information about authors and license of the source code, see the uploaded files. For instructions on how to use this artifact, please see README.md included in the artifact.

Artifact: Code-Specify-Test-Debug-Prove: Flexibly Integrating Separation Logic Specification into Conventional Workflows

Zenodo (CERN European Organization for Nuclear Research) · 2026-04-17

This artifact (the Docker Image) contains the following components: our tools (CN, Fulminate, and Darcy), verification results for the pKVM hyp allocator, and an Android Linux with the instrumented hyp allocator. For the most up-to-date versions, refer to the following repositories: CN, Fulminate, and Darcy Cut-out hyp allocator with specifications and proofs Fulminate-Instrumented Android Linux NOTE: the authors of the repository given above are the authors of the paper "Code-Specify-Test-Debug-Prove: Flexibly Integrating Separation Logic Specification into Conventional Workflows", for which this repository contains additional materials. For information about authors and license of the source code, see the uploaded files. For instructions on how to use this artifact, please see README.md included in the artifact.

Typing Strictness (Extended Version)

ArXiv.org · 2025-10-17 · 1 citations

Strictness analysis is critical to efficient implementation of languages with non-strict evaluation, mitigating much of the performance overhead of laziness. However, reasoning about strictness at the source level can be challenging and unintuitive. We propose a new definition of strictness that refines the traditional one by describing variable usage more precisely. We lay type-theoretic foundations for this definition in both call-by-name and call-by-push-value settings, drawing inspiration from the literature on type systems tracking effects and coeffects. We prove via a logical relation that the strictness attributes computed by our type systems accurately describe the use of variables at runtime, and we offer a strictness-annotation-preserving translation from the call-by-name system to the call-by-push-value one. All our results are mechanized in Rocq.

Developing Argumentation Skills in Middle School: Evidence From a Multilevel Growth Analysis

2025-01-01

Bennet: Randomized Specification Testing for Heap-Manipulating Programs

Proceedings of the ACM on Programming Languages · 2025-10-09

Property-based testing (PBT), widely used in functional languages and interactive theorem provers, works by randomly generating many inputs to a system under test. While PBT has also seen some use in low-level languages like C, users in this setting must craft all their own generators by hand, rather than letting the tool synthesize most generators automatically from types or logical specifications. For low-level code with complex memory ownership patterns, writing such generators can waste significant amounts of time. CN, a specification and verification framework for C, features a streamlined presentation of separation logic that is specially tuned to present only "easy" logical problems to an underlying constraint solver. Prior work on the Fulminate testing framework has shown that CN's streamlined specifications can also be checked effectively at run time, providing an oracle for testing whether a memory state satisfies a pre- or postcondition. We show that the restricted syntax of CN is also a good basis for deriving generators for random inputs satisfying separation-logic preconditions. We formalize the semantics for a DSL describing these generators, as well as optimizations that reorder when values are generated and propagate arithmetic constraints. Using this DSL, we implement a property-based testing tool, Bennet, that generates and runs random tests for C functions annotated with CN specifications. We evaluate Bennet on a corpus of programs with CN specifications and show that it can efficiently generate bug-revealing inputs for heap-manipulating programs with complex preconditions.