Implementing backward bounded model checking in CPAchecker

Backward bounded model checking is a technique for program analysis that aims to solve the error location reachability problem by searching for execution paths from an error location to the initial location and determining their feasibility, whereas regular forward techniques search for paths from the initial location to an error location. The main aim of this project will be to formulate the backward bounded model checking algorithm within the framework of CPA and develop an implementation in CPAchecker. This will also require figuring out which components already provide support for backward analysis in CPAchecker and developing support where it does not already exist. Once backward analysis is supported and the algorithm is implemented, it can be tested and benchmarked on a set of programs to evaluate its performance.