Code patches are the basic blocks of software evolution and thus recent testing and analysis techniques have started to focus on validating them. However, due to lack of specifications, most of these techniques focus on generic errors, such as crashes.

In this idea paper, we propose to adopt product programs, typically used to reason about hyperproperties and program equivalence, as a practical means of writing patch specifications. Such patch specifications could be partial, and they would benefit immediately from existing testing techniques such as fuzzing and symbolic execution.

Future work will investigate the feasibility of automatically generating product programs for real-world code patches, the ease of writing useful patch specifications, and the integration of such patch specifications with existing testing techniques and tools.