Patch Specifications via Product Programs

1@inproceedings{cadarPatchSpecificationsProduct2023,
2  author = {Cadar, Cristian and Schemmel, Daniel and Sharma, Arindam},
3  title = {Patch {{Specifications}} via {{Product}} {{Programs}}},
4  booktitle = {2023 {{International}} {{Conference}} on {{Formal}} {{Methods}} in {{Software}} {{Engineering}} {{(FormaliSE}} 2023)},
5  location = {Melbourne, Australia},
6  pages = {39--43},
7  year = {2023},
8  month = {may},
9  doi = {10.1109/FormaliSE58978.2023.00012},
10}

Code patches are the basic blocks of software evolution and several testing and analysis techniques have been proposed to validate them. However, due to lack of specifications, most of these techniques focus on generic errors, such as crashes.

In this vision paper, we propose to adopt product programs as a practical means of writing patch specifications that could be checked using existing testing techniques.

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.

Awards

• Our paper was awarded "Best Artifact" at FormaliSE 2023.