Reversing Programs for Error Reachability Analysis

Reachability analysis, used to determine whether an error location in a program is reachable from the initial state, is a key problem in software verification. While standard techniques typically perform this analysis in the forward direction, analyzing reachability backward from the error location can be more efficient in some instances. This research introduces a technique for reversing C programs, allowing existing forward reachability methods to effectively traverse the original program in reverse. The technique will be implemented as a standalone tool that can be easily integrated into the pipelines of existing verification tools.