                                          Property-Based Testing in Practice
               Harrison Goldstein                               Joseph W. Cutler                            Daniel Dickstein
            University of Pennsylvania                       University of Pennsylvania                         Jane Street
              Philadelphia, PA, USA                            Philadelphia, PA, USA                       New York, NY, USA
              hgo@seas.upenn.edu                               jwc@seas.upenn.edu                       ddickstein@janestreet.com

                                            Benjamin C. Pierce                        Andrew Head
                                          University of Pennsylvania            University of Pennsylvania
                                            Philadelphia, PA, USA                 Philadelphia, PA, USA
                                          bcpierce@seas.upenn.edu                 head@seas.upenn.edu

ABSTRACT                                                                    Python’s Hypothesis framework [37] had an estimated 500K users
Property-based testing (PBT) is a testing methodology where users           in 2021 according to a JetBrains survey [32]. Still, there is plenty of
write executable formal specifications of software components and           room for growth. Half a million Hypothesis users represent only 4%
an automated harness checks these specifications against many               of the total Python user base, whereas the Hypothesis maintainers
automatically generated inputs. From its roots in the QuickCheck            estimate [15] that the “addressable market” is at least 25%. (For
library in Haskell, PBT has made significant inroads in mainstream          comparison, the most popular testing framework, pytest, has 50%
languages and industrial practice at companies such as Amazon,              market share.)
Volvo, and Stripe. As PBT extends its reach, it is important to un-            To help move PBT toward wider adoption, the research commu-
derstand how developers are using it in practice, where they see            nity (ourselves included) needs to better understand the practical
its strengths and weaknesses, and what innovations are needed to            strengths and weaknesses of PBT and the places where further
make it more effective.                                                     technical advances are required. Existing work in the software engi-
    We address these questions using data from 30 in-depth inter-           neering literature has studied how other bug-finding tools are used
views with experienced users of PBT at Jane Street, a financial tech-       in practice (see §6), but PBT offers a unique set of tools and warrants
nology company making heavy and sophisticated use of PBT. These             its own investigation. Accordingly, we interviewed PBT users at
interviews provide empirical evidence that PBT’s main strengths             Jane Street, a financial technology firm that makes significant use
lie in testing complex code and in increasing confidence beyond             of PBT, to learn how they use PBT, where they see its value, and in
what is available through conventional testing methodologies, and,          what ways they think it might be improved. Concretely, we aimed
moreover, that most uses fall into a relatively small number of high-       to answer two main questions:
leverage idioms. Its main weaknesses, on the other hand, lie in the         RQ1: What are the characteristics of a successful and mature PBT
relative complexity of writing properties and random data genera-                culture at a software company?
tors and in the difficulty of evaluating their effectiveness. From these    RQ2: Are there opportunities for future work in the PBT space
observations, we identify a number of potentially high-impact areas              that are motivated by the needs of real developers?
for future exploration, including performance improvements, dif-
ferential testing, additional high-leverage testing scenarios, better       The first question aims both to offer guidance for engineers and
techniques for generating random input data, test-case reduction,           managers considering whether PBT might fit well in their organi-
and methods for evaluating the effectiveness of tests.                      zations and to provide a basis for evaluating and comparing PBT
                                                                            technologies. The second question aims to help shape further re-
1     INTRODUCTION                                                          search to maximize the impact of PBT.
                                                                               Our findings contribute a wide range of observations about de-
Property-based testing (PBT) is a powerful tool for evaluating soft-
                                                                            velopers’ experiences with PBT, adding nuance to the research
ware correctness. The process of PBT starts with a developer decid-
                                                                            community’s understanding of PBT’s real-world usage. Through
ing on a formal specification that they want their code to satisfy
                                                                            our interviews, we gleaned several new insights about the situa-
and encoding that specification as an executable property. An au-
                                                                            tions in which property-based tests are deployed in practice. We
tomated test harness checks the property against their code using
                                                                            found that developers use PBT mainly for testing components of
hundreds or thousands of random inputs, produced by a generator.
                                                                            complex systems, expecting the tests to provide greater confidence
If this process discovers a counterexample to the property—an input
                                                                            than conventional example-based unit tests yet still run quickly as
value that causes it to fail—the developer is notified.
                                                                            part of their normal test suite. Interestingly, we also found that de-
    The research literature is full of accounts of PBT successes, e.g.,
                                                                            velopers leverage PBT for the secondary benefit of communicating
in telecommunications software [2], replicated file [31] and key-
                                                                            specifications: properties serve as a form of persistent documen-
value [8] stores, automotive software [3], and other complex sys-
                                                                            tation, demonstrating the semantics of the software to readers—a
tems [30]. PBT libraries are available in most major programming
                                                                            benefit less commonly discussed in the literature. Finally, we found
languages, and some now have significant user communities—e.g.,
                                                                            that at Jane Street, PBT is primarily used in “high-leverage” sce-
ICSE 2024, April 2024, Lisbon, Portugal                                     narios, where properties are especially easy to identify and test.
2024.                                                                       Beyond deepening our understanding of when and why developers
ICSE 2024, April 2024, Lisbon, Portugal                            Harrison Goldstein, Joseph W. Cutler, Daniel Dickstein, Benjamin C. Pierce, and Andrew Head


reach for PBT, we also found that PBT technology can be improved             trees will be discarded, wasting precious generation time. A better
in several ways to better support developers. In particular, study           strategy is to hand-craft a generator that only produces valid BSTs,
participants reported struggling to generate distributions of test           but such generators can be nontrivial to write.
examples that they were convinced effectively exercised the prop-               If the property ever fails during testing, the failing value is pre-
erty, and sometimes viewed the process of designing random data              sented to the user. This value might be overly complex, with parts
generators as a distraction. They also lamented the lack of visible          that are irrelevant to the failure of the property, so most PBT frame-
feedback on the effectiveness of their testing.                              works provide tools for test-case reduction [36], usually called
   From these findings, we extract a list of opportunities for future        shrinking [29] in the PBT literature.
research, including understanding the nuances of PBT performance                The BST example above uses OCaml’s QuickCheck library, but
requirements, exploring better support for differential testing, and         the general approach—a module under test, a concise property, a
expanding the high-leverage scenarios in which PBT is most effec-            data generator, and a shrinker—is shared by all PBT tools, from
tive. We also highlight opportunities around improving languages             the original Haskell QuickCheck [11] to Python’s Hypothesis li-
for random data generators, designing interfaces for test-case reduc-        brary [37] and beyond. The power of PBT comes from the ability
tion (“shrinking”), evaluating testing success, and using developer          to test a huge number of system inputs with a single specification
feedback to improve the testing process.                                     and generator, often uncovering edge and corner cases that the
   We begin with background on PBT (§2), then present our study              developer might not have considered. It thus hits a useful midpoint
methodology and discuss of potential threats to validity (§3). We            between example-based unit tests and heavier-weight formal meth-
present the study’s main results (§4) and detail lessons learned in          ods, retaining the precision of traditional formal specifications and
the form of observations (§5.1) and research opportunities (§5.2)            their ability to characterize a system’s behavior on all possible in-
before discussing related work (§6) and concluding (§7).                     puts, but offering quick, best-effort validation instead of requiring
                                                                             developers to write formal proofs.
2    BACKGROUND                                                                  Of course, PBT is only one among many testing methodologies.
Properties are executable specifications of programs. For example,           Two primary alternatives are especially relevant to our study.
suppose a developer is working on a new implementation of binary                 Example-based unit testing [13] (as supported by pytest, JUnit,
search trees (BSTs)—tree structures where each internal node is              and other frameworks) evaluates a program by testing it on indi-
labeled with a data value that is greater than any labels in its left        vidual example inputs. For each input, the developer writes down a
subtree and less than any in its right subtree. They know that all the       short snippet of code that checks that the program’s output is cor-
operations on BSTs (insert, delete, etc.) must preserve this validity        rect for this input. (We call this style “example-based unit testing”
condition: given a valid BST, they should always produce a valid BST.        throughout the paper, rather than just “unit testing,” because PBT
To enforce this condition, they might write the following test for           is also typically used to test individual units within larger systems.)
the insert function using OCaml’s Core QuickCheck library [19]:                  Fuzz testing, invented by Miller [4, 39] and popularized by tools
    let test_insert_maintains_bst () =                                       like AFL [56], also aims to find bugs by randomly generating pro-
      QuickCheck . test                                                      gram inputs. The technical foundations of fuzz testing and PBT
        ( both int_gen ( filter valid_bst tree_gen ))                        overlap to a large (and increasing [34, 53]!) degree, but existing tools
        ( fun (x , t ) -> valid_bst ( insert t x ))                          from the two communities tend to be tuned for different situations:
                                                                             fuzz testing is typically used in integration testing of complete sys-
The second argument to QuickCheck.test (on the last line) is the             tems, to detect catastrophic bugs like crash failures and memory
property: It says, given an integer x and a BST t, that insert t x           unsafety, while PBT is used to flush out logical errors in smaller
should return a BST. The first argument to QuickCheck.test is a              software modules.
random data generator, which here generates a pair of both an int
and an arbitrary BST (obtained by generating an arbitrary binary
                                                                             3     METHODOLOGY
tree using tree_gen and using filter to discard trees that are not
valid BSTs). QuickCheck.test randomly generates hundreds or                  To address the research questions described in §1, we conducted an
thousands of pairs (x, t) and invoke the property to check each              interview study of developers who use PBT in their work. This study
pair. If this check ever fails, we have discovered a bug in insert.          was conducted in accordance with the ACM SIGSOFT Empirical
   Generators like tree_gen are usually written using an embedded            Standards for qualitative surveys.
domain specific language (eDSL) provided by the PBT framework,
which includes base generators like int_gen and combinators like             3.1     Population
both that can be used to create generators for complex data types            As the setting for our study, we chose Jane Street, a financial tech-
from generators for their parts. The generator language is embedded          nology firm that uses PBT extensively. We recruited 31 participants
in OCaml (in this case), giving generator writers access to the full         and carried out 30 interviews (one was a joint interview). Partici-
power of the host language. Generators can require some careful              pants were recruited by a Jane Street developer who volunteered
tuning to find bugs effectively. This is often because properties have       to coordinate the study: they found instances of PBT in the source
preconditions that define what it means for an input to be valid. For        tree and contacted the authors of those libraries; announced the
example, “filter valid_bst tree_gen” is a correct generator of               study on an internal blog; and carried out snowball sampling by
BSTs: it simply discards trees until tree_gen happens to generate            asking participants for others we should talk to. All participants
a valid BST. However, this means that the majority of the generated          had some experience with PBT, and most self-reported as having
Property-Based Testing in Practice                                                                             ICSE 2024, April 2024, Lisbon, Portugal


Table 1: Participant backgrounds. Columns 3–5 reflect op-                    Jane Street’s overall financial operations are supported by a di-
tional questions; participants that didn’t respond to these               verse set of software engineering efforts. We spoke to developers
are listed at the bottom. ★Measured in years. ★★Stated com-               working on core data structures, distributed systems, compilers,
fort with PBT on a Likert scale: 7 most comfortable, 1 least.             graphical interfaces, statistical computation, and even custom hard-
† Participant indicated skepticism of PBT. ‡ Pair interview;
                                                                          ware. Study participants spanned fifteen teams in four main areas:
coded as one participant. (At Jane Street’s request, we do not            Trading (2/30, across 2 teams), working directly with traders to
associate individuals with their teams or company divisions.)             develop technology specific to individual trading desks; Trading
                                                                          Infrastructure (13/30, across 5 teams), building platforms to sup-
    ID    Role       SE Exp.★ PBT Exp.★ Comfort★★                         port Jane Street’s trading; Quantitative Research (5/30, across 2
    1     Tester     12            3                                (6)   teams), writing software to enable research on trading algorithms;
    3     Maint. 22                17                               (7)   and Developer Infrastructure (11/30, across 6 teams), designing
    4     Maint. 15                16                               (6)   tools and languages upon which Jane Street’s applications are built.
    5     Tester     5             7                                (6)   Jane Street developers primarily work in OCaml, a programming
    6     Tester     16            16                               (7)   language with strong typing, good mechanisms for modularity,
    9     Tester     4             4                                (5)   and a focus on performance. OCaml is thought of as a functional
    11    Maint. 10                7                                (6)   language, but it has strong support for imperative programming as
    14    Tester     8             7                                (5)   well.
    15    Tester     2             2                                (6)
    16    Tester     8             8                                (3)   3.2    Protocol
    18    Tester     1             1                                (5)   We conducted a semi-structured one-hour interview with each
    20† Tester       5             2                                (5)   participant; Goldstein and Cutler led the interviews. For testers, the
    23    Tester     6             6                                (5)   prompts were:
    25‡ Testers 26                 20                               (5)      (1) Tell us about a noteworthy time that you applied PBT.
    26    Tester     2             2                                (6)         (a) What kinds of properties did you test?
    28    Tester     7             1                                (5)         (b) How did you generate test inputs?
    29    Tester     4             5                                (6)         (c) How did you evaluate the effectiveness of your testing?
      Other Testers: 2, 7, 8, 10, 12, 13, 17, 19† , 21, 22, 24, 27, 30          (d) What did you do to shrink your failing inputs?
                                                                             (2) Which parts of the PBT process are the most difficult?
                                                                             (3) What role does PBT play in your development workflow?
positive experiences. We also explicitly asked for participants who          (4) To whom would you recommend PBT?
reported neutral or negative feelings about PBT, but they were               (5) In what contexts is PBT most useful?
difficult to find: most felt they did not have enough experience to          (6) Is there anything that would make PBT more useful to you?
speak to those feelings. Two self-described PBT-critical developers
participated in the study. More details about the study participants      The script was designed to attain depth by encouraging reflection
can be found in Table 1.                                                  on real, memorable experiences with PBT. It evolved somewhat
   Most of those we interviewed were testers (26/30), who use PBT         over the course of the study, allowing us to validate interesting or
tools in their day-to-day work, but we also spoke to several main-        unexpected observations from earlier interviews.
tainers (4/30) who play a role in building and maintaining Jane              A separate script was used with maintainers:
Street’s PBT infrastructure. These two groups were given different           (1) Have you seen the type of adoption that you want from your
prompts (see below), reflecting our expectation that the maintain-                PBT tools?
ers would be able to offer a more “global” perspective, but their            (2) How can QuickCheck be improved?
responses were coded uniformly since they address the same re-               (3) What do you think it would take to get everyone at Jane
search questions.                                                                 Street using PBT? Would that be a good thing?
   Participants who answered an optional background question-                (4) What do you hope we’ll learn from this study?
naire had between 1 and 26 years of professional Software Engineer-       Time permitting, we also asked maintainers about their use of PBT.
ing experience (median 7) and between 1 and 20 years using PBT               We did not explicitly interview until saturation; we simply tried
(median 6). This wide range of experience (for PBT, almost as wide        to recruit a reasonably sized group that was representative of PBT
as possible, since the first paper on PBT is only 23 years old! [11])     users at the company. However, as we neared the end of the study
also means we heard from developers at many different points in           we felt we were no longer learning about new aspects or perspec-
their careers and with differing levels of software development           tives on PBT, and we saw convergence on many of our findings (as
experience. When asked to rate their comfort with PBT on a Likert         evidenced by the numbers we report in §4). Thus, we do not expect
scale, these participants were overall quite comfortable with PBT         there are significant holes in our results.
(median 6 out of 7): all but one were at least “somewhat comfortable”        Once the interviews were complete, they were transcribed using
(5 out of 7). Working with developers who are already relatively          an automated transcription service [42] and analyzed to extract im-
fluent users of PBT allowed us to benefit from their well-informed        portant themes following a thematic analysis process [7]. Goldstein
ideas about how to make PBT better, as well as their frustrations         and Cutler carried out an open coding pass (reading through the
and challenges.                                                           transcripts and assigning thematic codes as they went). The codes
ICSE 2024, April 2024, Lisbon, Portugal                            Harrison Goldstein, Joseph W. Cutler, Daniel Dickstein, Benjamin C. Pierce, and Andrew Head


we chose focused on participant goals, benefits of PBT, challenges          50,000 places across the code base” to establish reliable behavioral
encountered, and opportunities for improvement. Once the set of             contracts for library consumers (P13). Another participant used
codes stabilized, they were validated by a third co-author, then clar-      PBT to check software that interacted with information they were
ified by the whole team to obtain a final set of clean codes. Finally,      “sending to the [stock] exchange” (P25), which, should it contain
one co-author performed an axial coding pass (reading through               errors, could incur serious financial costs. An advantage of PBT
the transcripts and codes again to make connections and ensure              in these cases was its ability to explore edge cases (mentioned by
consistency) with the updated codebook. Our codebook is available           10/30) since, in the words of one participant, “the bugs are always
online1 .                                                                   going to happen in cases you didn’t think of” (P21).
                                                                               For many participants, PBT served to increase confidence that
3.3     Threats to Validity                                                 their software was robust. They described code tested with PBT as
While our study covered a wide variety of software teams and tasks,         “solid” (P6, P28), and some (9/30) explicitly mentioned that PBT in-
it should be noted that participants mostly described using a single        creased their “confidence” that the code was correct. One described
PBT toolset, in a single language and software development ecosys-          using PBT when they “wanted peace of mind” (P11). Confidence
tem. Our findings may under-represent the usage patterns and                was accompanied by material evidence of success: a third of partic-
challenges experienced by those working with other PBT toolsets             ipants (10/30) said their property-based tests found bugs that they
in other languages. To help us develop findings that generalize             had not found via other methods.
beyond the Jane Street toolset, we designed our interview protocol             A less obvious benefit of PBT was its ability to help participants
to focus considerable attention on the conceptual and methodolog-           better understand their work. One participant described properties
ical aspects of PBT, rather than on details of OCaml’s QuickCheck           as tools that “force [the developer] to think clearly” (P30) about
implementation or specifics of how it is used at Jane Street. (In the       their code, and another pointed out that sometimes properties fail
cases where we make observations that are toolset-specific, e.g.,           because the specification (rather than the code) is wrong (P10).
where we know tools outside of OCaml address some of the prob-              In such cases, failing tests can highlight gaps in the developer’s
lems we observed, we state this explicitly.) In addition, participants      understanding of the problem space that could lead to issues later.
were mostly experienced developers who were comfortable with                   Outside of the testing loop, properties were useful for docu-
PBT. This means that our study under-reports the experiences of             mentation and communication (12/30). One participant noted that
novice developers. Finally, as discussed above, we did not measure          properties “are part of the interface and part of the documentation”
saturation as interviews progressed, so there is a chance that more         (P3) and emphasized that, unlike other documentation, properties
interviews may still have uncovered new insights.                           never fall out of date: whereas a textual description in a comment
    Another threat comes from the inherent limitations of inter-            might drift from the code’s actual behavior, a property is repeatedly
view studies. For one thing, participants may not always accurately         re-checked as the code changes. Many also talked about the value
recall the particulars of their experiences with tools. We did our          of PBT in the code review process (18/30) as a compact way to
best to mitigate this threat by asking developers to tell us about          express what a particular program does. One remarked: “I feel like
specific experiences—a standard technique for studies like ours.            [PBT] is very nice for review. . . I really dread seeing 10,000 lines of
Additionally, our own biases as interviewers may naturally have             tests where you just need to spend hours to read code and under-
skewed the results; Goldstein and Cutler, who carried out the inter-        stand what’s going on. . . And I think, if there is a QuickCheck test
views, and Pierce and Head, who also participated with additional           and you look at the property that’s been tested, which is usually
questions, are all property-based testing researchers who have a            much shorter. . . it gives you much more confidence that the code is
vested interest in the outcome of the study. Outcomes that show             correct.” (P19)
PBT in a positive light may have unintentionally been highlighted,             The benefits of PBT were such that even those who were critical
and criticisms that we have addressed in our prior work may have            of it found it to be beneficial in some situations. During the recruit-
received extra attention.                                                   ing process we tried to explicitly recruit participants who said they
                                                                            did not like PBT; we found two (P19 and P20), but the criticism
4     RESULTS                                                               in their interviews turned out to be constructive suggestions that
We now present our findings. We start by describing the benefits            were echoed by PBT’s proponents as well, and both primarily spoke
that PBT delivered to developers and how it fit with the other testing      about situations where PBT was valuable.
approaches they used. Then we describe in detail their experiences             Moreover, some participants who liked PBT really liked it: one
writing specifications, designing generators, debugging, and evalu-         said that they “use QuickCheck for everything” (P13) and another
ating testing success, focusing both on challenges they experienced         asserted that “everyone should be aware of it” (P27). Yet another
and on opportunities for improving PBT tools and workflows.                 participant argued that “[PBT] is so useful that it’s worth trying
                                                                            to reorganize your code into the form that it is applicable. PBT is
4.1     Benefits of PBT                                                     so helpful that if you can reinvent things that way, you should.”
                                                                            (P10) Several participants (8/30) also talked about evangelizing PBT,
As might be expected, the primary reason participants used PBT was
                                                                            encouraging others to use it and increasing its adoption across the
to assess whether their code was correct. Participants often used
                                                                            organization.
PBT to validate widely used or mission-critical code. For example,
                                                                               We found that this sort of evangelism benefited all parties: PBT
one participant described using PBT for code that was “used in
                                                                            becomes more useful as more people on a team or in an organization
1 https://doi.org/10.5281/zenodo.10407686                                   use it. A culture of supporting PBT can save work: P24 and P27
Property-Based Testing in Practice                                                                              ICSE 2024, April 2024, Lisbon, Portugal


both noted that PBT would be easier to use if more developers in            Expect tests and PBT were both used to test individual software
the organization provided generators for the types exported by           units during development. PBT was almost always described as
their modules, making it much easier to test code in other modules       running in Jane Street’s build system, and many developers actu-
that uses those types. In addition, treating property-based tests as     ally test their properties “locally after each edit” (P2) Participants
documentation, as many (12/30) did, requires that others in the          described strict time budgets for PBT—no more than “30 seconds”
organization can read and understand such documentation.                 (P27) and as low as “50 milliseconds” (P11)—to ensure it would not
                                                                         slow down the build. These time budgets serve to keep PBT from
                                                                         triggering the 1-minute-per-library timeout that many Jane Street
                                                                         developers set for their unit test suite (P7).
4.2     Comparisons to Other Testing Approaches                             Alongside these fast-turnaround unit testing tools, developers
The most common approach to testing at Jane Street is not PBT,           also used fuzzing tools like AFL [56] and AFL++ [20] for integration
but rather an example-based unit testing framework called “expect        testing. A third of participants (10/30) mentioned fuzzing, and a few
tests” [40]. Expect tests are basically conventional example-based       (3/30) described using AFL alongside PBT as part of their testing
unit tests with editor integration that helps developers create unit     process. In contrast to the strict timeouts set for expect and property-
tests from the outputs that the system produces. With expect tests,      based tests, one participant described a fuzzer that was forgotten
developers add code to the system under test that that logs in-          and left running for a year and a half on a spare server (P9). Others
teresting data to the standard output channel; the expect testing        did not run fuzzing this long, but still considered it to be running
framework then checks that the output matches the output string          “out of band” (P28), outside of the normal continuous integration
that was captured from the previous run of the system—it is up           and at time scales on the order of hours or days. The upshot is that
to the developer to decide which output is intended. Expect tests        fuzzing tools are given much longer to run than PBT tools.
are integrated into Jane Street’s editor workflow, and they are used
pervasively in much the same way as frameworks like pytest and
JUnit are used in other languages. Thus, we can use comparisons          4.3    Writing Specifications
with expect tests as a proxy for comparisons with example-based          The previous sections have dealt with PBT at a high level; we now
tests in general where the specifics of expect tests are not relevant.   begin a deeper dive into the specifics of the PBT process and how
    From a legibility perspective, PBT was sometimes seen as better,     developers described actually using PBT tools. The first step in this
sometimes worse than expect tests. Expect tests were described as        process is defining one or more properties to test. While participants
more transparent and “often easier to understand” (P5). P18 said         did describe struggling with this stage, many ultimately developed
“expect tests. . . explain what they’re doing to a better degree. And    powerful strategies for finding properties.
it’s easier for someone to come in and review my test,” and P27             Many participants (16/30) said the process of writing specifica-
made a similar point. But expect tests can sometimes go past from        tions slowed their progress. P4 summed it up like this: “I think the
“transparent” to just verbose. P17 complained that reading a whole       most common failure mode is actually not knowing what properties
output string was onerous, and another participant complained            to test.” Challenges ranged from systems that seemed not to have
“[with expect tests] it’s easy to get into a mode where you just like    properties at all—P1 talked about “a server that serves queries. . . and
write a test, and you just print out a bunch of crap. And then it’s      has some. . . nuanced behavior” that is not compatible with “logical
really annoying to like code review that test because there’s just       properties”—to systems whose properties were hard to articulate
too much stuff” (P7). Properties are more concise.                       in the form of QuickCheck tests: “With [example-based unit tests],
    PBT and expect tests also present different strengths and weak-      I kind of look at it, I can just make a snap judgment as to whether
nesses when it comes to test writing. One participant said that          this is okay or not. Trying to formalize that judgment sometimes
writing an individual expect test is “way easier than writing invari-    can be very difficult.” (P2)
ants,” but they highlighted that at the scale of a whole test suite         Challenges in articulating properties can come from the way code
they “love not writing specific unit tests cases” (P13).                 is written. P7 explained that mutable state (e.g., a hidden variable
    Ultimately there was no universal preference for properties or       that may change between calls to the same function) gets in the way
expect tests—both should be available in a developer’s toolkit. We       of writing properties: “there’s. . . this hidden state component. . . that
might infer from participant responses that when code is simple          kind of makes it harder for me to think about what are the right
enough and examples communicate its behavior well enough, ex-            laws.” P22 also pointed out that “integrating the outside world
pect tests are an attractively lightweight option. In cases where        and. . . dealing with the interaction of very large and complicated
the code is particularly difficult to get right or where writing out     systems” makes it less clear how to “meaningfully test with PBT.”
enough examples becomes tedious, it seems PBT may be a better            (These findings are not surprising. It is well known that code that
choice.                                                                  interacts with its environment is also a challenge for testing in
    One area where properties seem to be at a clear advantage over       general, not just PBT: stateful code uses mutable data structures
expect tests is in the confidence they provide developers. P25 re-       such as hash tables, which might introduce differences between
marked of Jane Street developers that “[they] go to randomized           runs of the same test if the state is not reset properly; and effectful
testing when [they’re] not so confident of what [they’ve] done.”         code might rely on external files, databases, or networks, which
As discussed above, around a third of participants talked directly       may not be safe to access over and over during testing.)
about PBT building confidence, and the same proportion reported             Despite these difficulties, the developers we spoke to were gener-
PBT finding bugs that had not been found with other methods.             ally enthusiastic about PBT. One might therefore wonder: Did they
ICSE 2024, April 2024, Lisbon, Portugal                              Harrison Goldstein, Joseph W. Cutler, Daniel Dickstein, Benjamin C. Pierce, and Andrew Head


simply forge ahead regardless, or did they have specific techniques            4.4     Generating Test Data
for circumventing the difficulties of writing specifications?                  Participants had several goals for generating inputs. First and fore-
    What we found was that developers often succeeded in apply-                most, many participants (17/30) talked about needing to generate
ing PBT by being opportunistic in their choice of when to apply                values that satisfy some precondition. This can be extremely impor-
it. Rather than try to apply PBT to every program at all times,                tant for effective testing: if too few of the generated values satisfy
participants looked for situations where it offered high leverage:             the property’s precondition, then testing will fail to exercise the
more confidence for less work. Some participants described this in             code in interesting ways; in the worst case, it may even report false
general terms as “go[ing] for the low hanging fruit” (P2) or finding           positives. A few of the preconditions mentioned by participants
places where “the properties are sort of obvious” (P28), but many              are easy to satisfy randomly—for example non-empty strings or
enumerated specific situations where they would reach for PBT.                 lists—but most are quite hard to satisfy: valid postal addresses, well-
    Classical Properties (11/30). Certain forms of properties are fa-          structured XML documents, red-black trees, and syntactically valid
miliar from the PBT literature and from library documentation for              S-expressions are extremely unlikely to be generated by a naïve ran-
PBT frameworks. These include mathematical properties (e.g., the               dom generator. Participants also described test data requirements
commutativity of addition), properties drawn from CS theory (e.g.,             going beyond precondition validity. Some (5/30) said they wanted
repeated sorting has no effect), and properties that naturally fall            their test data to be “realistic”—i.e., similar to the distributions of
out of a data structure’s invariants (e.g., the ordering condition of a        data the application was likely to see in the real world. Others de-
BST). These properties may be more accessible because they are                 scribed heuristics for the distribution of the input data, for example
naturally top-of-mind.                                                         generating lists or trees of a “reasonable size” (P9).
    Round-Trip Properties (11/30) are also common in the literature;               Participants described a few different ways that they generated
we heard about them so much more often than the other classical                inputs. Most talked about either handwritten random generators
cases that they seem worth calling out on their own. These proper-             (19/30), which are the default approach in libraries like QuickCheck,
ties check that a pair of functions are inverses of one another—for            or derived generators (19/30), which are inferred based on the types
example, parsing and pretty-printing or encoding and decoding                  of the data to be generated (e.g., the type int list implies a generic
functions. This situation is easy to notice and easy to test since the         generator for lists of integers).
properties are incredibly succinct (you call one function, then its                The need for handwritten generators seemed to be a source of
inverse, and then check that the final result matches the original             friction for many participants. P6 said that writing generators for
input), so round-trip properties are a popular choice.                         data that satisfies property preconditions is “the biggest annoyance
    Catastrophic Failure Properties (7/30). Rather than write logical          with trying to use QuickCheck” and many participants thought
specifications, some participants used PBT to try to provoke cata-             of writing generators as “tedious” (6/30) or “high-effort” (7/30). P2
strophic failures such as assertion failures and uncaught exceptions.          described the task of writing generators as intruding into their de-
In general, these kinds of properties provide less confidence in code          velopment process and contributing to a general perception of PBT
quality (there can still be logical errors, even if the code does not          as “high cost and low value.” Since PBT was usually described as an
crash), but they help to rule out worst-case scenarios and they are            integral part of the development process, rather than as a separate
easy to write. (These kinds of specifications are identical to the ones        quality-assurance task, it makes sense that requiring detours into a
often used for fuzzing; the line between the techniques is blurry,             lengthy generator design process might make PBT less desirable.
but since the participants were using PBT tools—including complex                  Besides requiring significant effort to use, available tools for writ-
generators—and testing small units of software, we still consider              ing generators by hand do not easily enable developers to produce
this relevant for our purposes.)                                               precondition-satisfying values that are also well distributed in the
    Differential Properties (17/30). A “differential property” (in sense       way they would like. Writing a precondition-satisfying generator
of differential testing [25]) compares the system under test to a              on its own can be a large task—whole papers have been written
reference implementation of the same functionality that serves as              about generators for a single complex data type [43]—and account-
a specification; these are often also called model-based properties            ing for distributional considerations adds even more friction. P13
(c.f. model-based testing [54]), especially when the reference imple-          said, “there’s a tension in. . . all these handwritten generators be-
mentation is designed to be an abstract model of the original code.            tween ‘I want kind of coverage of everything’ and ‘I want coverage
Differential properties were by far the most widely implemented                that is realistic for most inputs.’” As a solution, P13 suggested that
kind of property. Differential properties were described as a “natural         one might be able to carefully combine two different handwritten
place to use property based testing” (P3)—indeed, one participant              generators to achieve these competing goals, but thought “that way
remarked that PBT was challenging in a particular situation in part            lies madness”. Other participants had an idea of the kinds of values
because a good reference implementation was not available (P1).                they wanted to generate more or less frequently, but they were
    The common theme of the high-leverage scenarios described                  not sure how to get there: “What should [the probabilities in my
above is the availability of a succinct abstraction that can be used           generator] look like?. . . I’m sure if I studied probability and statis-
in writing a property. These PBT scenarios were summed up by                   tics and fully understood how the QuickCheck generating system
P9 with the following mantra: “[PBT is] most useful when. . . you              worked, I could give better guesses. But all my guesses. . . they’re
have a really good abstraction with a complicated implementation.”             not educated guesses. They’re just random. . . And that’s a little bit
We discuss how these high-leverage scenarios should be taken into              of a mental strain.” (P20)
account to accelerate research in PBT in §5.
Property-Based Testing in Practice                                                                                ICSE 2024, April 2024, Lisbon, Portugal


   In Jane Street’s ecosystem, derived generators are enabled via          intermediate values that were found during shrinking. P1 said “the
the ppx_quickcheck library, which provides a preprocessor that             shrinker gets it right. . . but [it’s] still useful to see the evolution.”
runs before the compiler and synthesizes generator code from type
information. Ideally, this approach is totally automatic, providing a
generator without any additional user input, and it was described          4.6    Understanding Success
fondly by participants. Many included it in their workflows (19/30),       Property-based testing not only requires a developer to understand
and one called it “f***ing amazing” (P5). P13 went so far as to suggest    test failures; it also requires developers to understand whether
that “you shouldn’t really be handwriting generators, you should           passing a test actually means the software is correct. If the inputs
be changing the structure of your type [to improve generation].”           provided by the test harness fail to adequately exercise buggy code,
(For example, if a function being tested takes an int flag but the         a property-based test may pass misleadingly. One participant de-
only valid values are 0, 1, and 2, then replacing int with an appro-       scribed this situation, recalling a bug in published code that their
priate enumerated type causes ppx_quickcheck to derive a better            property-based tests failed to catch because the generator was “not
generator.) Others (7/30) leveraged a combination of derived and           generating the case that [they] had in mind” (P19). P14 worried
handwritten generators, using derived generators as a foundation           they could not trust their generators because they had “no idea
on which to build more complex generator programs.                         what it’s generating.” (P14)
   For both handwritten and derived generators, Jane Street devel-            But, while participants understood that, in principle, tests could
opers recognized opportunities for tool improvements. P4 described         pass erroneously, 11 of them—more than a third—said they did not
the process of hand-writing a generator for a mutable data structure       think as hard as they should about testing effectiveness, or whether
as “overwhelming,” and P6 suggested that libraries could do a better       they had adequately tested their software with their generators.
job supporting that use case. As for improving PPX-derived genera-         Some (3 of the 11) reported seeing their property catch a couple
tors, P26 wanted better support for generating values of generalized       of bugs and deciding that they did not have to improve their prop-
algebraic data types (GADTs), special types in OCaml and some              erties any further; the rest trusted that the generators provided
other languages that can express fine-grained properties of data.          by OCaml’s QuickCheck library or the ones they derived or wrote
                                                                           themselves would be good enough. While this group is a minority
                                                                           of our sample, even a signal of this size is striking: PBT tools such
4.5     Understanding Failure                                              as derived generators should make it easy for developers to get
Debugging is often tricky, but participants described ways that            started; they should not (but evidently sometimes do) discourage
tracking down bugs detected by PBT can be especially so. One               developers from being critical of their test suite.
participant described their debugging process: after finding a large,         On the other hand, several participants described techniques for
unwieldy counter-example with PBT, “you have to pull that failure          validating their PBT tests:
into a separate sort of regression test. . . which runs the same infras-      Mutation Testing (7/30). Some participants intentionally added
tructure but does it with much more detail. . . Having done that, it       bugs to their code and checked that their tests successfully found
is still sometimes unclear—like what about this example actually           those bugs. This technique is standard in the testing literature [44,
causes us to fail?” (P1) This is an instance of a broader problem:         47] and used in testing benchmarks such as Magma [27] and Etna [50].
random test generators often produce failing examples that are                Example Inspection (8/30). An even simpler way to assess a gen-
too large to make sense of during debugging. To help developers            erator’s distribution is to look at a handful of examples that the
understand failing examples, PBT frameworks offer shrinkers that           generator produces; one participant (P26) even designed a small
transform large inputs into smaller inputs that (presumably) intro-        utility to graphically render one example at a time, to make them
duce the same bug. One participant in our study deemed shrinking           easier to understand at a glance.
“necessary” (P15), and two who implemented their own ad-hoc PBT               Code Coverage (2/30). Participants evaluated the code coverage
frameworks (P8 and P21) insisted that shrinking was one of the             achieved by their tests and used code coverage measurements as
most important features they implemented.                                  an indication that their properties were thoroughly exploring the
   That said, participants found it difficult to use the shrinking         space of program behaviors.
functionality in QuickCheck, which resembles shrinking in many                Property Coverage (1/30). Another participant measured coverage
PBT frameworks. In such frameworks, shrinking is achieved by               not of the system under test, but of the property itself. This is a
having users manually write functions that incrementally reduce a          weaker measurement, since it does not say anything about the
large value (e.g., a string, list, or other more complex data structure)   system under test, but it is much easier to make because it can be
to a smaller one that triggers the same failure. Participants saw          measured without complex tooling.
writing shrinkers as an undesirable activity: one plainly stated, “I          A couple of participants (2/30) compensated for gaps in their
hate writing shrinkers” (P4). One challenge of writing shrinkers           property-based tests by supplementing them with example-based
was writing them in a way that preserved important non-trivial             unit tests. In these cases, example-based tests were written to test
invariants: “It’s easy to write a shrinker that accidentally does not      complementary functionality that could not be easily tested with
preserve some invariant, and that makes your test fail.” (P13) This        properties. As one participant put it, “it’s kind of not a good idea to
led one participant to ask for a “generic solution [for shrinking],        use QuickCheck in isolation” (P6), as doing so limits the breadth of
rather than having the user write shrinkers” (P10).                        software behaviors that can be tested.
   A few participants also described wanting more information                 How might PBT frameworks provide better support these (and
from the shrinking process—for example, the progressively smaller          other) techniques that give insight into how thoroughly properties
ICSE 2024, April 2024, Lisbon, Portugal                                Harrison Goldstein, Joseph W. Cutler, Daniel Dickstein, Benjamin C. Pierce, and Andrew Head


have been tested? P15 described their ideal interaction with PBT                 part of their testing toolbox, using it to gain confidence when they
tools, where the tools give “insight into what [PBT] is doing. . . I             were unsure of code’s correctness, especially where correctness
think a combination of knowing what it’s doing and having more                   was of critical importance. PBT gave them confidence that their
control of the space that it’s exploring would be interesting.” Partici-         software was operating correctly, finding bugs in code that had not
pants desired greater awareness of what their tools were doing: P16              been found via other methods.
called this “visibility”, and P30 called it “inspectability.” Many par-          OB2: Properties are used as devices for communicating specifications.
ticipants wanted greater visibility to better understand the breadth             Tests are generally a valuable form of documentation, and proper-
of inputs generated. P18, for instance, desired “visualization of the            ties are no exception. Jane Street developers use them as executable
test [inputs] being generated”. Others wished to see details such                evidence that code satisfies a specification, which has significant ad-
as “the answer [of the function under test] on a smaller set of ex-              vantages over traditional documentation that might go stale as the
amples” (P9), “statistics on. . . edge cases” (P18), statistics describing       code changes. As shown in §4.1 and §4.2, properties were deemed
generated inputs such as “the average length of [a generated] list”              especially useful for communication during code review: when
(P25), and code coverage (P9).                                                   properties were available, they were considered a strong signal that
                                                                                 the code was correct, and when unavailable reviewers sometimes
4.7     Tradeoffs                                                                asked the submitter to write some. These auxiliary uses for proper-
As the earlier sections indicate, using PBT is not without costs.                ties are worth keeping in mind for PBT framework designers; for
From coming up with properties to evaluating testing success, par-               example, some property languages try to make properties easier to
ticipants found friction in many steps of PBT. Participants described
seeing themselves as employing PBT more often if its “overhead”
could be lowered (P26), or if there was less “effort necessary to
integrate [it] into [their] workflow” (P10).                                                                  Observations
   Amidst these costs, PBT was often seen as worth the effort. For                    OB1      Property-based testing is being used successfully
some participants, development of properties was unremarkable.                                 to build confidence in complex systems.
For others with more involved implementation, it was still worth
                                                                                      OB2      Properties are used as devices for communicating
the costs: in the words of P6,“[It was] a huge slog, but I was like
                                                                                               specifications.
‘this needs to be right,’ and. . . I’m glad I did it.” P17 describes the
tradeoffs of using PBT as follows: “doing PBT is both putting in                      OB3      Property-based tests need to be fast; they are
more effort and saving oneself effort as well.”                                                expected to perform as well as other unit tests.
                                                                                      OB4      Property-based testing is used opportunistically
5     LESSONS LEARNED                                                                          in high-leverage scenarios where properties are
In this section we answer our research questions, setting a course                             readily available; developers rarely go out of
for upcoming PBT research and tool development that is grounded                                their way to write subtle specifications.
in findings from the study. Our recommendations cut across the                        OB5      Developers see writing generators as a distrac-
PBT process, and establish new goals and priorities for different                              tion, preferring to use derived generators.
areas of PBT research. We first answer RQ1 with observations of                       OB6      Developers may not interrogate properties that
PBT’s practice that offer a reality check to PBT researchers and tool-                         do not find bugs, even in cases where they ac-
builders (§5.1), then we answer RQ2 with a technical and empirical                             knowledge they should.
research agenda motivated by our study (§5.2).
                                                                                                        Research Opportunities
5.1     The State of Practice
                                                                                      RO1      Understand time constraints for property-based
Recall that RQ1 asks, “What are the characteristics of a successful                            tests.
and mature PBT culture at a software company?” Based on the
                                                                                      RO2      Improve support for differential and model-based
results of our study, we answer: A mature PBT culture considers
                                                                                               testing.
PBT a tool to be opportunistically applied in situations of high
leverage to gain confidence in software and document its behavior;                    RO3      Make more testing scenarios high leverage.
developers try to keep PBT “out of their way,” expecting it to work                   RO4      Streamline the process of writing well-
quickly and easily. In this section, we synthesize the results from                            distributed, precondition-satisfying generators.
the previous section into observations that expand on these ideas.                    RO5      Improve interfaces for shrinking.
Some observations point forward to §5.2, where we present ideas                       RO6      Improve tools for evaluating testing effective-
for future research based on our findings.                                                     ness.
OB1: Property-based testing is being used successfully to build confi-                RO7      Connect evaluation of testing effectiveness and
dence in complex systems. The broader research community some-                                 generator improvement.
times situates PBT as a lower-effort, lower-reward alternative to
formal proofs of correctness, but that perspective underestimates
PBT as a practical tool for improving software quality. In §4.1, we
show that the developers at Jane Street found PBT to be a valuable                             Figure 1: Summary of major outcomes.
Property-Based Testing in Practice                                                                            ICSE 2024, April 2024, Lisbon, Portugal


write by providing terse syntax and expressive defaults, but those        Instead, as seen in §4.4, many participants opted to test with gener-
features may cause problems if they hurt readability.                     ators derived from the types of the data that their programs operate
                                                                          on.
OB3: Property-based tests need to be fast; they are expected to perform      This has two implications. First, it means that ongoing work to-
as well as other unit tests. The PBT literature is not always clear       wards improving generator automation is critical. After all, as easy
about exactly when in the software engineering process they expect        as current derived generators are to use, they are not always suffi-
properties to be written, but in §4.2 we observe that PBT’s niche is      cient. The well-liked ppx_quickcheck library, for example, cannot
testing module-level code during development. This is in contrast         derive generators for properties with complex preconditions. Broad-
with fuzz testing, which, when used by Jane Street developers, is         ening applicability of derived generators lowers barriers to using
treated as a separate step and run outside of the standard testing        PBT. Second, it means that developers of manually written genera-
workflow. This discrepancy makes sense in view of the differing           tor languages must carefully consider any added friction. Languages
goals that we observed for PBT and fuzzing: PBT is used for module-       that make generators more difficult to write, perhaps because do-
level tests with often-complex logical specifications, while fuzzing      ing so enables desirable new features, should be cautious—these
is used for integration-style tests of whole applications, to check       features may be unlikely to see adoption.
for relatively basic (e.g., assertion failure or uncaught exception)         Separately, languages and tools for writing generators should
errors. (Look ahead to RO1 in §5.2.)                                      provide a wealth of sensible defaults, and they should optimize the
   Properties live alongside other unit tests, so they are expected       user experience around common patterns. Participants indicated
to run as quickly as other unit tests. Knowing this may change            that there was room for improvement in all of these areas, at least
priorities for some PBT researchers. If users are only testing their      in OCaml’s QuickCheck. (Look ahead to RO4 in §5.2.)
properties for 50 milliseconds, research advances that increase input
generation or property execution speed might make the difference          OB6: Developers may not interrogate properties that do not find bugs,
between bugs being found or not. Conversely, approaches that make         even in cases where they acknowledge they should. A passing prop-
generators more thorough but significantly slower may not be used         erty sometimes means that a program is free of bugs, but it may also
unless developers are given reason to accept longer execution times.      mean that the input values are not the right ones to trigger a latent
                                                                          bug. Developers acknowledged this fact, and they had expectations
OB4: Property-based testing is used opportunistically in high-leverage    around the kinds of input values that they wanted when testing
scenarios where properties are readily available; developers rarely go    their properties. (Besides satisfying property preconditions, they
out of their way to write subtle specifications. Conventional wisdom      wanted them to be realistic, well-distributed in the space, inter-
in the PBT community sometimes assumes that developers decide             esting enough to cover corner and edge cases, and more.) But, as
to use PBT and then try to think of a specification, but the study        shown in §4.6, when it came time to decide if their generators met
participants generally did the opposite: they saw an obvious testable     expectations, developers did not analyze them closely. Developers
property and then decided to use PBT. We call situations with these       of PBT frameworks, and especially PBT automation, should keep
readily available properties “high-leverage” testing scenarios.           this in mind: automated tools for generating test inputs risk giving
   The high-leverage scenarios varied—we are not confident that           developers a false sense of security. They must ensure that their
we have documented all of the ones available in practice—but a few        tools test thoroughly, because testers may not. (Look ahead to RO6
are described in §4.3. The most popular was differential or model-        in §5.2.)
based testing, which compares the code under test to some other
available implementation. (We are not surprised our participants          5.2    Research Opportunities
found these techniques useful, after all both differential and model-     Now we tackle RQ2: “What opportunities exist for future work in
based testing have rich literatures on their own, but we did not          the PBT space, motivated by the needs of real developers?” Based on
expect to see them so seamlessly incorporated into PBT workflows.)        our results, we conclude: Exciting avenues for PBT research include
Other high-leverage properties include round-trip properties that         further studies into performance and usability of PBT generators,
check an inverse relationship between functions and catastrophic          broader and deeper support of high-leverage PBT scenarios, better
failure properties that make sure a program does not fail completely.     tools for shrinking, and better visibility into the testing process.
   What does this opportunistic use of PBT mean for researchers           This section discusses research opportunities in software engineer-
and tool builders? Frameworks can optimize for and automate these         ing, programming languages, and human-computer interaction
scenarios—tools like Hypothesis Ghostwriter [16] have already             research that will unlock the yet-unrealized potential of PBT. Some
begun incorporating common PBT scenarios into an automation               research opportunities point backward to §5.1, where we synthesize
framework—improving the common case and accelerating PBT use              observations that inform these ideas.
even further. High-leverage scenarios should also be incorporated
into PBT benchmarks like Etna [50] to make sure that the perfor-          RO1: Understand time constraints for property-based tests. Future
mance of PBT algorithms is evaluated in a way that reflects their         studies should more thoroughly explore how long developers across
use in real-world scenarios. (Look ahead to RO2 and RO3 in §5.2.)         the software industry actually budget for running PBT. In this
                                                                          study, we heard about numbers between 50 milliseconds and 30
OB5: Developers see writing generators as a distraction, preferring       seconds; that difference is massive, and tools that support PBT
to use derived generators. Since PBT is often done in the midst of        cannot make optimal decisions around optimization without clearer
development, developers are reluctant to slow down and write a            data. Furthermore, future research should develop a sense of how
generator; the task was seen as both difficult and time-consuming.        long is “enough” for common kinds of properties and software so
ICSE 2024, April 2024, Lisbon, Portugal                            Harrison Goldstein, Joseph W. Cutler, Daniel Dickstein, Benjamin C. Pierce, and Andrew Head


tools have the data to argue for larger time budgets where required.         continue to look for ways to use current active-tuning strategies
Moreover, developers of tools that combine ideas from PBT and                for pre-tuning (e.g., by saving inputs to be run later) and ways to
fuzzing need to carefully examine their performance and recognize            make pre-tuned generators easier to use (e.g., with interfaces that
that many PBT users set strict timeouts that may preclude the                help developers write complex generators).
overhead of measuring code coverage while running tests. This is                 When it comes to precondition-satisfying generators, many seek
encouraging for tools like Crowbar [17] and HypoFuzz [26] that               to unify languages for writing generators with ones for writing
allow developers to transition between short-running PBT and                 preconditions. One approach, used in the QuickChick PBT frame-
longer-running fuzzing with the same properties. (See OB3 in §5.1.)          work [46], uses inductive relations as a language for both properties
RO2: Improve support for differential and model-based testing. As            and generators [35, 45]. This approach works well in the Coq proof
the most popular high-leverage scenario for PBT, differential test-          assistant, but complex inductive relations are not expressible in
ing seems particularly interesting as a topic of further research.           mainstream languages or accessible to non-specialists. Researchers
Differential testing has a rich literature, as discussed in §6, but          should consider ways to generalize these results. Alternatively, ded-
in the context of PBT there are still advances within reach. For             icated languages such as ISLa [53] use a common language that
example, in languages like OCaml with rich module structures,                is closer to the logical connectives one might use in a standard
researchers should aim to increase automation around differential            programming language; more research should be done to evaluate
testing and produce a test harness for comparing modules without             if this approach can be applied in common PBT scenarios. Whatever
requiring any manual setup; Hypothesis Ghostwriter has begun to              dual-purpose language is chosen, this is a compelling path forward.
incorporate similar ideas with Python’s classes. (See OB4 in §5.1.)          (See OB5 in §5.1.)

RO3: Make more testing scenarios high leverage. Some testing situa-          RO5: Improve interfaces for shrinking. It is clear from the study
tions are just barely outside the realm of “high-leverage” scenarios,        results that shrinkers would be far more useful if they were both
and improved tooling could make the difference. For example, P5              more automated and more informative. As we mention above, we
described a technique that they used to test a poorly abstracted             recommend that existing frameworks improve automation by in-
module with an overly complicated interface: instead of writing              corporating internal test-case reduction [36, 52], which uses gener-
normal properties, they instrumented the module with log state-              ators to aid in shrinking, where possible. Internal shrinking has the
ments, wrote properties about what those logs should look like,              added benefit of always producing valid values, which is difficult
and then tested the module via an external interface that hides              to achieve otherwise.
many of its internal details. Generalizing and operationalizing this             Participants also asked to see more intermediate examples from
technique—e.g., perhaps with temporal logic in the style of Quick-           the shrinking process. Indeed, there are cases where the smallest
strom [41]—would allow for better testing leverage in cases where            failing example is not the most helpful one: e.g., if the shrinker
poor abstraction prevents traditional PBT.                                   outputs the tuple (0, 0), one might conclude that any tuple of
   Other testing situations might be supported better as well. Po-           integers triggers the bug, but it may be that the bug is only found
tential opportunities include improving PBT support for code with            if the first component is actually 0. This example motivated Hy-
mutable state (e.g., by saving memory snapshots for repeatable               pothesis to begin developing a tool that will give users a variety of
tests) and code that interacts with the environment (e.g., via robust        tools for exploring failing tests. Debugging cases using shrinking
integration with tools for mocking [38]). Increasing the scenarios in        might mean showing many shrunk examples to the user, following
which PBT works out of the box will naturally make it higher-value           related work in the model-finding literature [14, 18], or even provid-
for developers. (See OB4 in §5.1.)                                           ing control over the shrinking process (e.g., with novel interactions
                                                                             allowing the user to click on components of a value to shrink only
RO4: Streamline the process of writing well-distributed, precondition-
                                                                             those components).
satisfying generators. This has been a research goal for the PBT
community since the beginning. Our study clarifies some promising            RO6: Improve tools for evaluating testing effectiveness. Participants
paths forward, including improving tools for automated tuning,               reported ad-hoc, piecemeal approaches to understanding their test-
generalizing unified languages for defining generators alongside             ing effectiveness, and they asked for better ways to visualize test-
properties, and supporting alternatives to randomness as first-class.        ing feedback. As a simple first step, tools should always announce
   There are two main options for tuning generator distributions.            counts of discarded test cases (i.e., ones that failed the property’s
Actively tuned generators modify their distribution live, in re-             precondition) so the developer can catch problems early. Many PBT
sponse to feedback, whereas pre-tuned generators compute dis-                tools provide some way to aggregate statistics while a property is
tributions ahead of time. Actively tuned generators are the norm             running (see Haskell QuickCheck’s label and collect functions)
in the fuzzing literature [20] and have been ported to PBT in many           but OCaml’s QuickCheck hides output when tests succeed, which
forms [17, 23, 34, 48], but they spend precious testing time on tuning       obscures that information, and more should be done around the
analysis, making them less useful in time-constrained PBT scenar-            usability and legibility of these kinds of aggregations. Going further,
ios. Pre-tuned generators can be much faster, but they currently             participants desired (1) better interfaces for scanning through ex-
require too much programmer effort. For example, reflective genera-          amples of generated values, (2) better ways of visualizing generated
tors [22] (which build on example-based tuning à la the Inputs from          distributions, and (3) better integration of code and branch cov-
Hell approach [51]) automate the process of generating realistic             erage information. These could significantly improve developers’
test inputs, but this automation is only possible if a reflective gen-       understanding of how thoroughly their code has been tested. (See
erator is already available. Moving forward, the community should            OB6 in §5.1.)
Property-Based Testing in Practice                                                                              ICSE 2024, April 2024, Lisbon, Portugal


RO7: Connect evaluation of testing effectiveness and generator im-        Beller et al. coined the term “Test Guided Development” to describe
provement. How might a developer clearly express their test data          the strategy that programmers actually use. Our study agrees with
goals and ensure that the generator achieves them? Future tools           the idea that developers use testing to guide their thinking during
could tighten the feedback loop wherein a developer evaluates and         development (§4.1). We also corroborate challenges that another
then expresses how to improve their generator at the same time.           study found around integration testing: Greiler et al. [24] found
For instance, a future user interface might display a generator’s         that while unit testing is common, integration testing is difficult
distribution in some graphical form like a bar chart and allow the        and often left to the the software’s users; in our study, developers
developer to directly manipulate the distribution by dragging bars        struggled to use PBT for integration testing because it is difficult to
up and down. Alternatively, the developer might be able to click          write specifications of entire systems’ behaviors. (§4.3).
on those annotations to request that the distribution try harder to          Our study also suggests that PBT addresses testing difficulties
cover a particular line or balance a particular branch, in the style      raised in the literature. Aniche et al. [1] observed that developers
of AFLGo [10]. In an ideal world, an insufficient generator could be      try to write relatively “random” test cases, with the hope of acciden-
caught and fixed in a few clicks, without allowing bugs slip by.          tally stumbling on bugs; this is related to developers’ goals for PBT
                                                                          generators, discussed in §4.4, although PBT has the advantage of au-
                                                                          tomating this process in many cases. Another study [25], focusing
6    RELATED WORK                                                         on differential testing, found PBT to be a valuable tool in a devel-
We focus, in this section, on related work exploring the usability of     oper’s toolbox, providing a coherence check for important code;
testing and formal methods tools. Prior work on PBT, testing, and         however, they also found some problems with differential testing
formal methods usability has made important observations about            systems, such as naïve sampling algorithms that failed to trigger
the challenges of specification and bug finding, but it has lacked the    bugs and large counter-examples that were difficult to reason about.
depth and domain focus to paint a clear picture of PBT, its usage,        Our study suggests new tools may address these problems.
and opportunities for improvement.                                           Formal methods. PBT is sometimes described as a “lightweight
   Property-based testing. As a precursor to this study, our group did    formal method.” Indeed, a recent position paper [49] argued that
a smaller-scale pilot study with developers using Hypothesis [21].        testing techniques like PBT and fuzzing were important steps on
The full-scale study is far more in-depth, and presents more detailed     the way towards more formal verification. Formal methods as a
and nuanced findings, although talking to Python developers did           field have seen similar calls for usability improvements. A report
raise a few concerns that were less prevalent at Jane Street, espe-       out of the Naval Research Lab [28] says, “to be useful to software
cially when it comes to difficulty coming up with specifications.         practitioners, most of whom lack advanced mathematical training
   A study analyzing open-source libraries using Hypothesis [12]          and theorem proving skills, current formal methods need a number
evaluated the kinds of properties that developers test in practice,       of additional attributes, including more user-friendly notations,
and found significant overlap with our “high-leverage” testing sce-       completely automatic (i.e., pushbutton) analysis, and useful, easy
narios. In particular, they found that both round-trip and differential   to understand feedback.” This report was published in 1998, but, as
or model-based testing are overrepresented in real-world tests.           our study shows, some of their usability criteria are still not ade-
   An experience report from Amazon [9] described differential test-      quately met by modern PBT tools. A more contemporary account
ing as a major use-case of PBT and reported that developers used          agrees that “the user experience of formal methods tools has largely
shrinking tools for debugging and mutation testing to ensure test-        been understudied” [33] and calls for better education and tools for
ing effectiveness. Our study confirms these patterns and explores         writing and understanding specifications.
further PBT use-cases (§4.3), insights around shrinking (§4.5), and
concerns about testing effectiveness (§4.6).                              7   CONCLUSION
   Other studies highlight a more narrow set of specific challenges
                                                                          Our study reveals that, even after two decades of active exploration—
faced by developers using PBT. One experience report describing
                                                                          and, increasingly, exploitation—of PBT, there is still much to learn
PBT use at DropBox [31] cited usability problems when testing
                                                                          about how it is being used and what challenges it faces in practice.
timing-dependent code. The report found that sequences of timed
                                                                          We contribute a wealth of observations about PBT’s use in an
operations resist shrinking, often remaining unwieldy, and that
                                                                          industrial setting, along with well-founded ideas for future research
timing dependence caused tests to be flaky. An education-focused
                                                                          in PBT that that we, with the help of the broader community, hope
study using PBT [55] observed that the PBT community lacks good
                                                                          to pursue in the coming years.
motivating examples. While the former concern only appeared in
passing in our study (when discussing PBT’s handling of stateful
software), the latter—a dearth of good motivating examples—might          ACKNOWLEDGMENTS
be ameliorated by our characterization of high-leverage testing           We would like to thank John Hughes, Hila Peleg, Zac Hatfield-
scenarios in §5.                                                          Dodds, and Shriram Krishnamurthi for their input and feedback
   Testing more generally. Beyond PBT, there is considerable work         on drafts of this paper. Also, thank you to Ron Minsky and others
studying usability software of testing in general. Our study sheds        at Jane Street for being open to this kind of collaboration. We ap-
light into how these common testing issues manifest in PBT specif-        preciate the support of the University of Pennsylvania’s PLClub
ically. Two studies of developers who use IDEs [5, 6] conclude that       and Penn HCI. This work was financially supported by NSF awards
testing, especially Test Driven Development, is not as prevalent          #1421243, Random Testing for Language Design and #1521523, Expe-
as conventional wisdom would suggest. Based on these studies,             ditions in Computing: The Science of Deep Specification.
ICSE 2024, April 2024, Lisbon, Portugal                                             Harrison Goldstein, Joseph W. Cutler, Daniel Dickstein, Benjamin C. Pierce, and Andrew Head


REFERENCES                                                                                    [20] Andrea Fioraldi, Dominik Maier, Heiko Eißfeldt, and Marc Heuse. 2020. {AFL++}
 [1] Maurício Aniche, Christoph Treude, and Andy Zaidman. 2022. How Developers                     : Combining Incremental Steps of Fuzzing Research. https://www.usenix.org/
     Engineer Test Cases: An Observational Study. IEEE Transactions on Software                    conference/woot20/presentation/fioraldi
     Engineering 48, 12 (Dec. 2022), 4925–4946. https://doi.org/10.1109/TSE.2021.             [21] Harrison Goldstein, Joseph W Cutler, Adam Stein, Benjamin C Pierce, and Andrew
     3129889                                                                                       Head. 2022. Some Problems with Properties, Vol. 1. https://harrisongoldste.in/
 [2] Thomas Arts, John Hughes, Joakim Johansson, and Ulf Wiger. 2006. Testing tele-                papers/hatra2022.pdf
     coms software with quviq QuickCheck. In Proceedings of the 2006 ACM SIGPLAN              [22] Harrison Goldstein, Samantha Frohlich, Meng Wang, and Benjamin C. Pierce.
     workshop on Erlang (ERLANG ’06). Association for Computing Machinery, New                     2023. Reflecting on Random Generation. In Proceedings of ACM Programming
     York, NY, USA, 2–10. https://doi.org/10.1145/1159789.1159792                                  Languages. Seattle, WA, USA. https://doi.org/10.1145/3607842
 [3] Thomas Arts, John Hughes, Ulf Norell, and Hans Svensson. 2015. Testing AU-               [23] Harrison Goldstein and Benjamin C. Pierce. 2022. Parsing Randomness. Pro-
     TOSAR software with QuickCheck. In 2015 IEEE Eighth International Confer-                     ceedings of the ACM on Programming Languages 6, OOPSLA2 (Oct. 2022), 128:89–
     ence on Software Testing, Verification and Validation Workshops (ICSTW). 1–4.                 128:113. https://doi.org/10.1145/3563291
     https://doi.org/10.1109/ICSTW.2015.7107466                                               [24] Michaela Greiler, Arie van Deursen, and Margaret-Anne Storey. 2012. Test confes-
 [4] Karen Barrett-Wilt. 2021. The trials and tribulations of academic publishing – and            sions: A study of testing practices for plug-in systems. In 2012 34th International
     Fuzz Testing. https://www.cs.wisc.edu/2021/01/14/the-trials-and-tribulations-                 Conference on Software Engineering (ICSE). 244–254. https://doi.org/10.1109/
     of-academic-publishing-and-fuzz-testing/                                                      ICSE.2012.6227189 ISSN: 1558-1225.
 [5] Moritz Beller, Georgios Gousios, Annibale Panichella, Sebastian Proksch, Sven            [25] Muhammad Ali Gulzar, Yongkang Zhu, and Xiaofeng Han. 2019. Perception and
     Amann, and Andy Zaidman. 2019. Developer Testing in the IDE: Patterns, Beliefs,               Practices of Differential Testing. In 2019 IEEE/ACM 41st International Conference
     and Behavior. IEEE Transactions on Software Engineering 45, 3 (March 2019),                   on Software Engineering: Software Engineering in Practice (ICSE-SEIP). 71–80.
     261–284. https://doi.org/10.1109/TSE.2017.2776152                                             https://doi.org/10.1109/ICSE-SEIP.2019.00016
 [6] Moritz Beller, Georgios Gousios, Annibale Panichella, and Andy Zaidman. 2015.            [26] Zac Hatfield Dodds. 2023. HypoFuzz. https://hypofuzz.com/
     When, how, and why developers (do not) test in their IDEs. In Proceedings of             [27] Ahmad Hazimeh, Adrian Herrera, and Mathias Payer. 2021. Magma: A Ground-
     the 2015 10th Joint Meeting on Foundations of Software Engineering (ESEC/FSE                  Truth Fuzzing Benchmark. Proceedings of the ACM on Measurement and Analysis
     2015). Association for Computing Machinery, New York, NY, USA, 179–190.                       of Computing Systems 4, 3 (June 2021), 49:1–49:29. https://doi.org/10.1145/3428334
     https://doi.org/10.1145/2786805.2786843                                                  [28] Constance Heitmeyer. 1998. On the Need for Practical Formal Methods. Technical
 [7] Ann Blandford, Dominic Furniss, and Stephann Makri. 2016. Analysing Data.                     Report. https://apps.dtic.mil/sti/citations/ADA465485 Section: Technical Reports.
     In Qualitative HCI Research: Going Behind the Scenes, Ann Blandford, Dominic             [29] John Hughes. 2007. QuickCheck Testing for Fun and Profit. In Practical Aspects of
     Furniss, and Stephann Makri (Eds.). Springer International Publishing, Cham,                  Declarative Languages (Lecture Notes in Computer Science), Michael Hanus (Ed.).
     51–60. https://doi.org/10.1007/978-3-031-02217-3_5                                            Springer, Berlin, Heidelberg, 1–32. https://doi.org/10.1007/978-3-540-69611-7_1
 [8] James Bornholt, Rajeev Joshi, Vytautas Astrauskas, Brendan Cully, Bern-                  [30] John Hughes. 2016. Experiences with QuickCheck: Testing the Hard Stuff and
     hard Kragl, Seth Markle, Kyle Sauri, Drew Schleit, Grant Slatton, Serdar                      Staying Sane. In A List of Successes That Can Change the World: Essays Dedicated
     Tasiran, Jacob Van Geffen, and Andrew Warfield. 2021. Using lightweight                       to Philip Wadler on the Occasion of His 60th Birthday, Sam Lindley, Conor McBride,
     formal methods to validate a key-value storage node in Amazon S3. In SOSP                     Phil Trinder, and Don Sannella (Eds.). Springer International Publishing, Cham,
     2021.     https://www.amazon.science/publications/using-lightweight-formal-                   169–186. https://doi.org/10.1007/978-3-319-30936-1_9
     methods-to-validate-a-key-value-storage-node-in-amazon-s3                                [31] John Hughes, Benjamin C. Pierce, Thomas Arts, and Ulf Norell. 2016. Mysteries
 [9] James Bornholt, Rajeev Joshi, Vytautas Astrauskas, Brendan Cully, Bernhard                    of DropBox: Property-Based Testing of a Distributed Synchronization Service. In
     Kragl, Seth Markle, Kyle Sauri, Drew Schleit, Grant Slatton, Serdar Tasiran, Jacob            2016 IEEE International Conference on Software Testing, Verification and Validation
     Van Geffen, and Andrew Warfield. 2021. Using Lightweight Formal Methods                       (ICST). 135–145. https://doi.org/10.1109/ICST.2016.37
     to Validate a Key-Value Storage Node in Amazon S3. In Proceedings of the ACM             [32] JetBrains. 2021. Python Developers Survey 2021 Results. https://lp.jetbrains.com/
     SIGOPS 28th Symposium on Operating Systems Principles (SOSP ’21). Association                 python-developers-survey-2021/
     for Computing Machinery, New York, NY, USA, 836–850. https://doi.org/10.1145/            [33] Shriram Krishnamurthi and Tim Nelson. 2019. The Human in Formal Methods. In
     3477132.3483540                                                                               Formal Methods – The Next 30 Years (Lecture Notes in Computer Science), Maurice H.
[10] Marcel Böhme, Van-Thuan Pham, Manh-Dung Nguyen, and Abhik Roychoud-                           ter Beek, Annabelle McIver, and José N. Oliveira (Eds.). Springer International
     hury. 2017. Directed Greybox Fuzzing. In Proceedings of the 2017 ACM SIGSAC                   Publishing, Cham, 3–10. https://doi.org/10.1007/978-3-030-30942-8_1
     Conference on Computer and Communications Security (CCS ’17). Association for            [34] Leonidas Lampropoulos, Michael Hicks, and Benjamin C. Pierce. 2019. Coverage
     Computing Machinery, New York, NY, USA, 2329–2344. https://doi.org/10.1145/                   guided, property based testing. PACMPL 3, OOPSLA (2019), 181:1–181:29. https://
     3133956.3134020 event-place: Dallas, Texas, USA.                                              doi.org/10.1145/3360607
[11] Koen Claessen and John Hughes. 2000. QuickCheck: A Lightweight Tool for                  [35] Leonidas Lampropoulos, Zoe Paraskevopoulou, and Benjamin C. Pierce. 2017.
     Random Testing of Haskell Programs. In Proceedings of the Fifth ACM SIGPLAN                   Generating good generators for inductive relations. Proceedings of the ACM on
     International Conference on Functional Programming (ICFP ’00), Montreal, Canada,              Programming Languages 2, POPL (2017), 1–30. https://dl.acm.org/doi/10.1145/
     September 18-21, 2000, Martin Odersky and Philip Wadler (Eds.). ACM, Montreal,                3158133 Publisher: ACM New York, NY, USA.
     Canada, 268–279. https://doi.org/10.1145/351240.351266                                   [36] David R. MacIver and Alastair F. Donaldson. 2020. Test-Case Reduction via Test-
[12] Arthur Corgozinho, Marco Valente, and Henrique Rocha. 2023. How Developers                    Case Generation: Insights from the Hypothesis Reducer (Tool Insights Paper). In
     Implement Property-Based Tests. In Conference: 39th International Conference on               34th European Conference on Object-Oriented Programming (ECOOP 2020) (Leibniz
     Software Maintenance and Evolution (ICSME 2023).                                              International Proceedings in Informatics (LIPIcs), Vol. 166), Robert Hirschfeld and
[13] Ermira Daka and Gordon Fraser. 2014. A Survey on Unit Testing Practices and                   Tobias Pape (Eds.). Schloss Dagstuhl–Leibniz-Zentrum für Informatik, Dagstuhl,
     Problems. In 2014 IEEE 25th International Symposium on Software Reliability                   Germany, 13:1–13:27. https://doi.org/10.4230/LIPIcs.ECOOP.2020.13 ISSN: 1868-
     Engineering. 201–211. https://doi.org/10.1109/ISSRE.2014.11 ISSN: 2332-6549.                  8969.
[14] Natasha Danas, Tim Nelson, Lane Harrison, Shriram Krishnamurthi, and Daniel J.           [37] David R MacIver, Zac Hatfield-Dodds, and others. 2019. Hypothesis: A new
     Dougherty. 2017. User Studies of Principled Model Finder Output. In Software                  approach to property-based testing. Journal of Open Source Software 4, 43 (2019),
     Engineering and Formal Methods (Lecture Notes in Computer Science), Alessandro                1891. https://joss.theoj.org/papers/10.21105/joss.01891.pdf
     Cimatti and Marjan Sirjani (Eds.). Springer International Publishing, Cham, 168–         [38] Tim Mackinnon, Steve Freeman, and Philip Craig. 2000. Endo-testing: unit testing
     184. https://doi.org/10.1007/978-3-319-66197-1_11                                             with mock objects. Extreme programming examined (2000), 287–301.
[15] Zac Hatfield Dodds. 2022. current maintainer of Hypothesis (https://github.com/          [39] Barton P. Miller, Lars Fredriksen, and Bryan So. 1990. An Empirical Study
     HypothesisWorks/hypothesis). Personal communication.                                          of the Reliability of UNIX Utilities. Commun. ACM 33, 12 (dec 1990), 32–44.
[16] Zac Hatfield Dodds and David R. MacIver. 2023. Ghostwriting tests for you —                   https://doi.org/10.1145/96267.96279
     Hypothesis 6.82.0 documentation. https://hypothesis.readthedocs.io/en/latest/            [40] Minsky. 2015. Testing with expectations. https://blog.janestreet.com/testing-
     ghostwriter.html                                                                              with-expectations/
[17] Stephen Dolan and Mindy Preston. 2017. Testing with crowbar. In OCaml Work-              [41] Liam O’Connor and Oskar Wickström. 2022. Quickstrom: property-based accep-
     shop.                                                                                         tance testing with LTL specifications. In Proceedings of the 43rd ACM SIGPLAN
[18] Tristan Dyer, Tim Nelson, Kathi Fisler, and Shriram Krishnamurthi. 2022. Apply-               International Conference on Programming Language Design and Implementation
     ing cognitive principles to model-finding output: the positive value of negative              (PLDI 2022). Association for Computing Machinery, New York, NY, USA, 1025–
     information. Proceedings of the ACM on Programming Languages 6, OOPSLA1                       1038. https://doi.org/10.1145/3519939.3523728
     (April 2022), 79:1–79:29. https://doi.org/10.1145/3527323                                [42] Otter.ai. 2023. Otter.ai - Voice Meeting Notes & Real-time Transcription. https://
[19] Carl Eastlund. 2015. Quickcheck for Core.             https://blog.janestreet.com/            otter.ai/
     quickcheck-for-core/                                                                     [43] Michał H. Pałka, Koen Claessen, Alejandro Russo, and John Hughes. 2011. Testing
                                                                                                   an Optimising Compiler by Generating Random Lambda Terms. In Proceedings
                                                                                                   of the 6th International Workshop on Automation of Software Test (AST ’11). ACM,
Property-Based Testing in Practice                                                                                                   ICSE 2024, April 2024, Lisbon, Portugal


     New York, NY, USA, 91–97. https://doi.org/10.1145/1982595.1982615 event-place:          where they are. http://arxiv.org/abs/2010.16345 arXiv:2010.16345 [cs].
     Waikiki, Honolulu, HI, USA.                                                        [50] Jessica Shi, Alperen Keles, Harrison Goldstein, Benjamin C Pierce, and Leonidas
[44] M. Papadakis, M. Kintis, J. Zhang, Y. Jia, Y. L. Traon, and M. Harman. 2018.            Lampropoulos. 2023. Etna: An Evaluation Platform for Property-Based Testing
     Mutation Testing Advances: An Analysis and Survey. Advances in Computers                (Experience Report). Proc. ACM Program. Lang. 7 (2023). https://doi.org/10.1145/
     (Jan. 2018). http://dx.doi.org/10.1016/bs.adcom.2018.03.015                             3607860
[45] Zoe Paraskevopoulou, Aaron Eline, and Leonidas Lampropoulos. 2022. Comput-         [51] Ezekiel Soremekun, Esteban Pavese, Nikolas Havrikov, Lars Grunske, and An-
     ing correctly with inductive relations. In Proceedings of the 43rd ACM SIGPLAN          dreas Zeller. 2020. Inputs from Hell: Learning Input Distributions for Grammar-
     International Conference on Programming Language Design and Implementation              Based Test Generation. IEEE Transactions on Software Engineering (2020).
     (PLDI 2022). Association for Computing Machinery, New York, NY, USA, 966–980.           https://doi.org/10.1109/TSE.2020.3013716 Publisher: IEEE.
     https://doi.org/10.1145/3519939.3523707                                            [52] Jacob Stanley. 2017. Hedgehog will eat all your bugs. https://hedgehog.qa/
[46] Zoe Paraskevopoulou, Cătălin Hriţcu, Maxime Dénès, Leonidas Lampropoulos,          [53] Dominic Steinhöfel and Andreas Zeller. 2022. Input invariants. In Proceedings of
     and Benjamin C. Pierce. 2015. Foundational Property-Based Testing. In Inter-            the 30th ACM Joint European Software Engineering Conference and Symposium
     active Theorem Proving (Lecture Notes in Computer Science), Christian Urban             on the Foundations of Software Engineering (ESEC/FSE 2022). Association for
     and Xingyuan Zhang (Eds.). Springer International Publishing, Cham, 325–343.            Computing Machinery, New York, NY, USA, 583–594. https://doi.org/10.1145/
     https://doi.org/10.1007/978-3-319-22102-1_22                                            3540250.3549139
[47] Goran Petrovic and Marko Ivankovic. 2018. State of Mutation Testing at Google.     [54] Mark Utting and Bruno Legeard. 2010. Practical Model-Based Testing: A Tools
     In Proceedings of the 40th International Conference on Software Engineering 2017        Approach. Elsevier.
     (SEIP).                                                                            [55] John Wrenn, Tim Nelson, and Shriram Krishnamurthi. 2021. Using Relational
[48] Sameer Reddy, Caroline Lemieux, Rohan Padhye, and Koushik Sen. 2020. Quickly            Problems to Teach Property-Based Testing. The art science and engineering of
     generating diverse valid test inputs with reinforcement learning. In Proceedings        programming 5, 2 (Jan. 2021). https://doi.org/10.22152/programming-journal.org/
     of the ACM/IEEE 42nd International Conference on Software Engineering (ICSE             2021/5/9
     ’20). Association for Computing Machinery, New York, NY, USA, 1410–1421.           [56] Michał Zalewski. 2022. American Fuzzy Lop (AFL). https://github.com/google/
     https://doi.org/10.1145/3377811.3380399                                                 AFL original-date: 2019-07-25T16:50:06Z.
[49] Alastair Reid, Luke Church, Shaked Flur, Sarah de Haas, Maritza Johnson, and
     Ben Laurie. 2020. Towards making formal methods normal: meeting developers
