SPLASH 2025
Sun 12 - Sat 18 October 2025 Singapore
co-located with ICFP/SPLASH 2025
Sat 18 Oct 2025 12:00 - 12:15 at Orchid East - Type 2 Chair(s): Richard A. Eisenberg

Property-based testing is a popular technique for automatically testing semantic properties of a program, specified as a pair of pre- and post-conditions. The efficacy of this approach depends on being able to quickly generate inputs that meet the precondition, in order to maximize the set of program behaviors that are probed. For semantically rich preconditions, purely random generation is unlikely to produce many valid inputs; when this occurs, users are forced to manually write their own specialized input generators. One common problem with handwritten generators is that they may be \emph{incomplete}, i.e., they are unable to generate some values meeting the target precondition. This paper presents a novel program repair technique that patches an incomplete generator so that its range includes every valid input. Our approach uses a novel enumerative synthesis algorithm that leverages the recently developed notion of \emph{coverage types} to characterize the set of missing test values as well as the coverage provided by candidate repairs. We have implemented a repair tool for OCaml input generators, called Cobb, and have used it to repair a suite of benchmarks drawn from the property-based testing literature.

Sat 18 Oct

Displayed time zone: Perth change

10:30 - 12:15
Type 2OOPSLA at Orchid East
Chair(s): Richard A. Eisenberg Jane Street
10:30
15m
Talk
Borrowing From Session Types
OOPSLA
Hannes Saffrich University of Freiburg, Janek Spaderna University of Freiburg, Germany, Peter Thiemann University of Freiburg, Vasco T. Vasconcelos LASIGE, University of Lisbon
10:45
15m
Talk
Modal Effect Types
OOPSLA
Wenhao Tang The University of Edinburgh, Leo White Jane Street, Stephen Dolan Jane Street, Daniel Hillerström Category Labs and The University of Edinburgh, Sam Lindley University of Edinburgh, Anton Lorenzen University of Edinburgh
11:00
15m
Talk
On Higher-Order Model Checking of Effectful Answer-Type-Polymorphic Programs
OOPSLA
Taro Sekiyama National Institute of Informatics, Ugo Dal Lago University of Bologna & INRIA Sophia Antipolis, Hiroshi Unno Tohoku University
11:15
15m
Talk
Proof Repair across Quotient Type Equivalences
OOPSLA
Cosmo Viola University of Illinois Urbana-Champaign, Max Fan Cornell University, Talia Lily Ringer University of Illinois Urbana-Champaign
11:30
15m
Talk
Structural Information Flow: A Fresh Look at Types for Non-Interference
OOPSLA
Hemant Gouni Carnegie Mellon University, Frank Pfenning Carnegie Mellon University, USA, Jonathan Aldrich Carnegie Mellon University
Pre-print
11:45
15m
Talk
The Simple Essence of Overloading: Making ad-hoc polymorphism more algebraic with flow-based variational type-checking
OOPSLA
Jiří Beneš University of Tübingen, Jonathan Immanuel Brachthäuser University of Tübingen
DOI Pre-print
12:00
15m
Talk
We’ve Got You Covered: Type-Guided Repair of Incomplete Input Generators
OOPSLA
Patrick LaFontaine Purdue University, Zhe Zhou Purdue University, Ashish Mishra IIT Hyderabad, Suresh Jagannathan Purdue University, Benjamin Delaware Purdue University