Reference. Programmable Property-Based Testing
Property-based testing (PBT) is a popular technique for establishing confidence in software, where users write properties —i.e. executable specifications—that can be checked many times in a loop by a testing framework. In modern PBT frameworks, properties are usually written in shallowly embedded domain-specific languages, and their definition is tightly coupled to the way they are tested. Such frameworks often provide convenient configuration options to customize aspects of the testing process, but users are limited to precisely what library authors had the prescience to allow for when developing the framework; if they want more flexibility, they may need to write a new framework from scratch. We propose a new, deeper language for properties based on a mixed embedding that we call deferred binding abstract syntax , which reifies properties as a data structure and decouples them from the property runners that execute them. We implement this language in Rocq and Racket, leveraging the power of dependent and dynamic types, respectively. Finally, we showcase the flexibility of this new approach by implementing a variety of property runners in a shared framework, highlighting domain-specific testing improvements that can be unlocked by more programmable testing.
Cite
Cites 50 works (2 here)
With notes (2)
Finding and Understanding Bugs in C Compilers yangFindingUnderstandingBugs
Compilers should be correct. To improve the quality of C compilers, we created Csmith, a randomized test-case generation tool, and spent three years using it to find compiler bugs. During this period we reported more than 325 previously unknown bugs to compiler developers. Every compiler we tested was found to crash and also to silently generate wrong code when presented with valid input. In this paper we present our compiler-testing tool and the results of our bug-hunting study. Our first contribution is to advance the state of the art in compiler testing. Unlike previous tools, Csmith generates programs that cover a large subset of C while avoiding the undefined and unspecified behaviors that would destroy its ability to automatically find wrong-code bugs. Our second contribution is a collection of qualitative and quantitative results about the bugs we have found in open-source C compilers.
Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages carette-2009-finally
We have built the first family of tagless interpretations for a higher-order typed object language in a typed metalanguage (Haskell or ML) that require no dependent types, generalized algebraic data types, or postprocessing to eliminate tags. The statically type-preserving interpretations include an evaluator, a compiler (or staged evaluator), a partial evaluator, and call-by-name and call-by-value continuation-passing style (CPS) transformers. Our principal technique is to encode de Bruijn or higher-order abstract syntax using combinator functions rather than data constructors. In other words, we represent object terms not in an initial algebra but using the coalgebraic structure of the λ-calculus. Our representation also simulates inductive maps from types to types, which are required for typed partial evaluation and CPS transformations. Our encoding of an object term abstracts uniformly over the family of ways to interpret it, yet statically assures that the interpreters never get stuck. This family of interpreters thus demonstrates again that it is useful to abstract over higher-kinded types.
External (48)
- Property-Based Testing in Practice (2024)
- QuickerCheck: Implementing and Evaluating a Parallel Run-Time for QuickCheck (2024)
- falsify: Internal Shrinking Reimagined for Haskell (2023)
- Embedding by Unembedding (2023)
- Don’t Go Down the Rabbit Hole: Reprioritizing Enumeration for Property-Based Testing (2023)
- Etna: An Evaluation Platform for Property-Based Testing (Experience Report) (2023)
- Property-Based Fuzzing for Finding Data Manipulation Errors in Android Apps (2023)
- Testing Database Engines via Query Plan Guidance (2023)
- A Novel Coverage-guided Greybox Fuzzing based on Power Schedule Optimization with Time Complexity (2022)
- Parsing randomness (2022)
- Program adverbs and Tlön embeddings (2022)
- Deeper Shallow Embeddings (2022)
- Do Judge a Test by its Cover (2021)
- Generative type-aware mutation for testing SMT solvers (2021)
- Boosting fuzzer efficiency: an information theoretic perspective (2020)
- Test-Case Reduction via Test-Case Generation: Insights from the Hypothesis Reducer (Tool Insights Paper) (2020)
- AFL++: combining incremental steps of fuzzing research (2020)
- RackCheck: Property-Based Testing for Racket (2020)
- Coverage-Based Greybox Fuzzing as Markov Chain (2019)
- Coverage guided, property based testing (2019)
- JQF: coverage-guided property-based testing in Java (2019)
- Semantic Fuzzing with Zest (2019)
- Validity Fuzzing and Parametric Generators for Effective Random Testing (2019)
- FuzzFactory: domain-specific fuzzing with waypoints (2019)
- Interaction trees: representing recursive and impure programs in Coq (2019)
- Hedgehog: Release with Confidence (2019)
- PerfFuzz: automatically generating pathological inputs (2018)
- Random Testing for Language Design (PhD dissertation) (2018)
- Directed Greybox Fuzzing (2017)
- Generating good generators for inductive relations (2017)
- FairFuzz: A Targeted Mutation Strategy for Increasing Greybox Fuzz Testing Coverage (2017)
- Targeted property-based testing (2017)
- SlowFuzz: Automated Domain-Independent Detection of Algorithmic Complexity Vulnerabilities (2017)
- Crowbar: Property Fuzzing for OCaml (2017)
- Hypothesis: Property-Based Testing for Python (2016)
- Foundational Property-Based Testing (2015)
- Splittable pseudorandom number generators using cryptographic hashing (2013)
- Swarm testing (2012)
- Test-case reduction for C compiler bugs (2012)
- Giving Haskell a promotion (2012)
- Parametric higher-order abstract syntax for mechanized semantics (2008)
- Simplifying and Isolating Failure-Inducing Input (2002)
- QuickCheck: a lightweight tool for random testing of Haskell programs (2000)
- Building domain-specific embedded languages (1996)
- Experience with Embedding Hardware Description Languages in HOL (1992)
- Bolero: A fuzzing and property testing front-end framework for Rust
- HypoFuzz: Adaptive fuzzing of Hypothesis tests
- SQLancer: Automated testing to find logic and performance bugs in database systems