Dynamic automated program repair (APR) techniques have promising results, which use test suites for bug localization and evaluating candidate patches. Several studies have shown that generated patches by dynamic APR tools that pass its test suite do not always correctly implement the program’s expected behavior, which is known as test overfitting. My research aims to provide fresh insight into the test overfitting problem by using formal methods.