PV3 ⊧ AllRepairproposes minimal repairs to the source code to satisfy properties

Application domain/field

• Fault localization
• Automated program repair

Type of tool

Program repair

Expected input

Format:

C program, assertions written as __CPROVER_assert(..)

Expected output

List of all minimal repairs such that all assertions are true.

Internals

SMT solver

Comments

Mutation-based repair tool for C programs equipped with assertions The proposed repairs are minimal in the number of changes applied to the program code.