ICFP/SPLASH 2025
Sun 12 - Sat 18 October 2025 Singapore

We describe our effort on using property-based testing to test the OCaml 5 multicore runtime system. In particular, we cover three case studies of increasing complexity that utilize a model-based state machine framework: (a) Testing the Array module, (b) testing weak hash sets, and (c) testing the garbage collector, with the latter two behaving non-deterministically from the point of view of the
black-box testing process. We evaluate the approach empirically by analyzing the bugs found, and discuss both limitations of the approach and challenges we have met underway.