Talk: Property-Based Testing for the People
Harry Goldstein: Victor Basili Postdoc, University of Maryland, and (joint) Postdoc, University of Pennsylvania
Event Details
LIVE STREAM: https://uwmadison.zoom.us/j/95190450241?pwd=77azcjdiRaAkKMDRk76MvbtV2L5Snb.1
Abstract: Property-based testing (PBT) is a testing methodology that allows users to write executable specifications of programs and then test those specifications with automatically generated program inputs. PBT is well-documented as a power-tool for bug-finding, with success stories at companies like Amazon, Jane Street, DropBox, and Volvo, but it still has significant room to grow. My work combines techniques from programming languages, human-computer interaction, and software engineering to better understand the needs of real PBT users and increase the reach of this powerful testing tool.
In my talk, I’ll discuss three projects from my dissertation work, plus one ongoing project. I’ll start by motivating some core PBT challenges through the lens of real users’ experiences. Next, I’ll discuss theoretical PBT contributions, in particular free generators, which form the basis of a number of follow-on projects that improve random data generation for PBT. I’ll conclude discussing prior work by describing Tyche, an user interface for evaluating property-based testing effectiveness. My ongoing research explores how to use techniques from program synthesis to make testing easier; I’ll demonstrate a prototype system that uses a deductive synthesis algorithm to automate significant chunks of the PBT process.
Bio: Harry Goldstein is a Victor Basili Postdoctoral Fellow at the University of Maryland, and he holds a joint postdoctoral position at the University of Pennsylvania, where he earned his PhD in 2024. Harry's work combines programming languages, software engineering, and human-computer interaction to make it easier for developers to write safe and correct code. The main line of Harry's work focuses on property-based testing, a software testing paradigm that bridges the gap between standard unit testing and more heavy-weight formal methods.