bcp.bib

@preamble{{\newcommand{\SortNoop}[1]{}}}

@article{goldstein2023reflecting:old,
  title = {Reflecting on Random Generation},
  author = {Goldstein, Harrison and Frohlich, Samantha and
                  Wang, Meng and Pierce, Benjamin C.},
  journal = {Proceedings of the ACM on Programming Languages},
  number = {ICFP},
  year = {2024},
  bcp = {Yes},
  plclub = {Yes},
  keys = {types},
  note = {To appear}
}

@article{cutler2024stream,
  title = {Stream Types},
  author = {Joseph W. Cutler and Christopher Watson and
                  Phillip Hilliard and Harrison Goldstein and
                  Caleb Stanford and Benjamin C. Pierce},
  journal = {Proceedings of the ACM on Programming Languages},
  number = {PLDI},
  year = {2024},
  url = {https://arxiv.org/abs/2307.09553},
  bcp = {Yes},
  plclub = {Yes}
}

@inproceedings{Goldstein2024ICSE,
  title = {Property-Based Testing in Practice},
  author = {Harrison Goldstein and Joseph W. Cutler and
                  Daniel Dickstein and Benjamin C. Pierce and Andrew Head},
  year = {2024},
  booktitle = {International Conference on Software Engineering (ICSE)},
  url = {https://harrisongoldste.in/papers/icse24-pbt-in-practice.pdf},
  bcp = {Yes},
  plclub = {Yes}
}

@misc{Pierce:TFP24,
  author = {Benjamin C. Pierce},
  title = {delta: Ordered Types for Stream Processing},
  day = 10,
  month = jan,
  year = 2024,
  note = {Talk at Trends in Functional Programming (TFP)},
  plclub = {Yes},
  bcp = {Yes},
  slides = {http://www.cis.upenn.edu/~bcpierce/papers/2024-TFP-talk.pdf},
  keys = {types}
}

@misc{Pierce:POPL24ClimateTalk,
  author = {Benjamin C. Pierce},
  title = {},
  day = 17,
  month = jan,
  year = 2024,
  note = {Short talk at POPL reception},
  plclub = {Yes},
  bcp = {Yes},
  slides = {http://www.cis.upenn.edu/~bcpierce/papers/2024-POPL-reception-talk.pdf},
  keys = {climate}
}

@inproceedings{goldstein_property-based_2024,
  address = {Lisbon, Portugal},
  series = {{ICSE} '24},
  title = {Property-{Based} {Testing} in {Practice}},
  volume = {187},
  copyright = {All rights reserved},
  isbn = {9798400702174},
  url = {https://doi.org/10.1145/3597503.3639581},
  doi = {10.1145/3597503.3639581},
  abstract = {Property-based testing (PBT) is a testing methodology where users write executable formal specifications of software components and an automated harness checks these specifications against many automatically generated inputs. From its roots in the QuickCheck library in Haskell, PBT has made significant inroads in mainstream languages and industrial practice at companies such as Amazon, Volvo, and Stripe. As PBT extends its reach, it is important to understand how developers are using it in practice, where they see its strengths and weaknesses, and what innovations are needed to make it more effective.
We address these questions using data from 30 in-depth interviews with experienced users of PBT at Jane Street, a financial technology company making heavy and sophisticated use of PBT. These interviews provide empirical evidence that PBT's main strengths lie in testing complex code and in increasing confidence beyond what is available through conventional testing methodologies, and, moreover, that most uses fall into a relatively small number of high-leverage idioms. Its main weaknesses, on the other hand, lie in the relative complexity of writing properties and random data generators and in the difficulty of evaluating their effectiveness. From these observations, we identify a number of potentially high-impact areas for future exploration, including performance improvements, differential testing, additional high-leverage testing scenarios, better techniques for generating random input data, test-case reduction, and methods for evaluating the effectiveness of tests.},
  language = {en},
  booktitle = {Proceedings of the {IEEE}/{ACM} 46th {International} {Conference} on {Software} {Engineering}},
  publisher = {Association for Computing Machinery},
  author = {Goldstein, Harrison and Cutler, Joseph W. and Dickstein, Daniel and Pierce, Benjamin C. and Head, Andrew},
  year = {2024},
  pages = {1--13},
  file = {Goldstein - 2023 - Property-Based Testing in Practice Codebook.pdf:/Users/harrison/Zotero/storage/XRH6XD6C/Goldstein - 2023 - Property-Based Testing in Practice Codebook.pdf:application/pdf},
  bcp = {Yes},
  plclub = {Yes},
  keys = {testing}
}

@inproceedings{10.1145/3654777.3676407,
  author = {Goldstein, Harrison and Tao, Jeffrey and Hatfield-Dodds, Zac and Pierce, Benjamin C. and Head, Andrew},
  title = {Tyche: Making Sense of PBT Effectiveness},
  year = {2024},
  isbn = {9798400706288},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  url = {https://doi.org/10.1145/3654777.3676407},
  doi = {10.1145/3654777.3676407},
  abstract = {Software developers increasingly rely on automated methods to assess the correctness of their code. One such method is property-based testing (PBT), wherein a test harness generates hundreds or thousands of inputs and checks the outputs of the program on those inputs using parametric properties. Though powerful, PBT induces a sizable gulf of evaluation: developers need to put in nontrivial effort to understand how well the different test inputs exercise the software under test. To bridge this gulf, we propose Tyche, a user interface that supports sensemaking around the effectiveness of property-based tests. Guided by a formative design exploration, our design of Tyche supports developers with interactive, configurable views of test behavior with tight integrations into modern developer testing workflow. These views help developers explore global testing behavior and individual test inputs alike. To accelerate the development of powerful, interactive PBT tools, we define a standard for PBT test reporting and integrate it with a widely used PBT library. A self-guided online usability study revealed that Tyche’s visualizations help developers to more accurately assess software testing effectiveness.},
  booktitle = {Proceedings of the 37th Annual ACM Symposium on User Interface Software and Technology},
  articleno = {10},
  numpages = {16},
  keywords = {Randomized testing, multiple program executions, property-based testing (PBT), visual feedback},
  location = {Pittsburgh, PA, USA},
  series = {UIST '24},
  bcp = {Yes},
  plclub = {Yes},
  keys = {testing}
}

@misc{INT-talk-2024,
  author = {Hughes, John and Bannerjee, Rini and Pierce, Benjamin C.},
  title = {Adventures in Specification-Based Testing},
  note = {Invited talk at Isaac Newton Institute
                  Workshop on Big Specification:
                  Specification, Proof, and Testing at Scale},
  month = oct,
  slides = {http://www.cis.upenn.edu/~bcpierce/papers/Pierce-2024-INI-talk.pdf},
  year = 2024,
  bcp = {Yes},
  plclub = {Yes},
  keys = {testing}
}

@misc{FailFaster25,
  author = {Richey, Cynthia and Cutler, Joseph W. and Goldstein, Harrison and Pierce, Benjamin C.},
  title = {Fail Faster: Staging and Fast Randomness for High-Performance PBT},
  note = {Submitted to OOPSLA 2025},
  month = apr,
  paper = {https://www.cis.upenn.edu/~jwc/assets/fail-faster.pdf},
  year = 2025,
  bcp = {Yes},
  plclub = {Yes},
  keys = {testing}
}

@article{10.1145/3763082-old,
  author = {Tjoa, Ryan and Garg, Poorva and Goldstein, Harrison and Millstein, Todd
          and Pierce, Benjamin C. and Van den Broeck, Guy},
  title = {Tuning Random Generators: Property-Based Testing as Probabilistic Programming},
  year = {2025},
  issue_date = {October 2025},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  volume = {9},
  number = {OOPSLA2},
  url = {https://doi.org/10.1145/3763082},
  doi = {10.1145/3763082},
  journal = {Proc. ACM Program. Lang.},
  month = oct,
  articleno = {304},
  numpages = {28},
  keywords = {Automatic Differentiation, Probabilistic Programming, Property-Based Testing, Random Generation},
  bcp = {Yes},
  plclub = {Yes},
  keys = {testing},
  abstract = {Property-based testing validates software against an executable specification by evaluating it on randomly generated inputs. The standard way that PBT users generate test inputs is via generators that describe how to sample test inputs through random choices. To achieve a good distribution over test inputs, users must tune their generators, i.e., decide on the weights of these individual random choices. Unfortunately, it is very difficult to understand how to choose individual generator weights in order to achieve a desired distribution, so today this process is tedious and limits the distributions that can be practically achieved.    In this paper, we develop techniques for the automatic and offline tuning of generators. Given a generator with undetermined symbolic weights and an objective function, our approach automatically learns values for these weights that optimize for the objective. We describe useful objective functions that allow users to (1) target desired distributions and (2) improve the diversity and validity of their test cases. We have implemented our approach in a novel discrete probabilistic programming system, Loaded Dice, that supports differentiation and parameter learning, and use it as a language for generators. We empirically demonstrate that our approach is effective at optimizing generator distributions according to the specified objective functions. We also perform a thorough evaluation on PBT benchmarks, demonstrating that, when automatically tuned for diversity and validity, the generators exhibit a 3.1-7.4x speedup in bug finding.}
}

@article{10.1145/3764115,
  author = {Aamer, Zain K and Pierce, Benjamin C.},
  title = {Bennet: Randomized Specification Testing for Heap-Manipulating Programs},
  year = {2025},
  issue_date = {October 2025},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  volume = {9},
  number = {OOPSLA2},
  url = {https://doi.org/10.1145/3764115},
  doi = {10.1145/3764115},
  bcp = {Yes},
  plclub = {Yes},
  keys = {testing},
  abstract = {Property-based testing (PBT), widely used in functional languages and interactive theorem provers, works by randomly generating many inputs to a system under test. While PBT has also seen some use in low-level languages like C, users in this setting must craft all their own generators by hand, rather than letting the tool synthesize most generators automatically from types or logical specifications. For low-level code with complex memory ownership patterns, writing such generators can waste significant amounts of time. CN, a specification and verification framework for C, features a streamlined presentation of separation logic that is specially tuned to present only "easy" logical problems to an underlying constraint solver. Prior work on the Fulminate testing framework has shown that CN's streamlined specifications can also be checked effectively at run time, providing an oracle for testing whether a memory state satisfies a pre- or postcondition. We show that the restricted syntax of CN is also a good basis for deriving generators for random inputs satisfying separation-logic preconditions. We formalize the semantics for a DSL describing these generators, as well as optimizations that reorder when values are generated and propagate arithmetic constraints. Using this DSL, we implement a property-based testing tool, Bennet, that generates and runs random tests for C functions annotated with CN specifications. We evaluate Bennet on a corpus of programs with CN specifications and show that it can efficiently generate bug-revealing inputs for heap-manipulating programs with complex preconditions.},
  journal = {Proc. ACM Program. Lang.},
  month = oct,
  articleno = {413},
  numpages = {30},
  keywords = {Property-based Testing, Random Testing, Separation Logic}
}

@misc{Tuning25:old,
  author = {Tjoa, Ryan and
                  Garg, Poorva and
                  Goldstein, Harrison and
                  Millstein, Todd and
                  Pierce, Benjamin C. and
                  Van den Broeck, Guy },
  title = {Tuning Random Generators: Property-Based Testing as Probabilistic Programming},
  note = {Submitted to OOPSLA 2025},
  month = apr,
  year = 2025,
  bcp = {Yes},
  plclub = {Yes},
  keys = {testing}
}

@misc{IU-talk-2026,
  author = {Pierce, Benjamin C.},
  title = {Properties for the People},
  note = {Invited talk at IU Luddy School of Informatics,
                  Computing, and Engineering 25th Anniversary Symposium},
  month = feb,
  slides = {http://www.cis.upenn.edu/~bcpierce/papers/2026-IU-PftP2.pdf},
  year = 2026,
  bcp = {Yes},
  plclub = {Yes},
  keys = {testing}
}

@misc{topos-talk-2026,
  author = {Pierce, Benjamin C.},
  title = {Properties for the People},
  note = {Topis Institute Colloquium},
  month = feb,
  day = 26,
  video = {https://www.youtube.com/watch?v=4E0a-bZyIpM},
  year = 2026,
  bcp = {Yes},
  plclub = {Yes},
  keys = {testing}
}