PV3 AllRepairproposes minimal repairs to the source code to satisfy properties

Application domain/field

Type of tool

Program repair

Expected input


C program, assertions written as __CPROVER_assert(..)

Expected output

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


SMT solver


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.
C Program repair SMT



Related papers

Last publication date

14 July 2020

Related tools

Automated repair tools: Angelix, GenProg, FoRenSiC, Maple

ProVerB specific

ProVerB is a part of SLEBoK. Last updated: February 2023.