Backward bounded model checking (BBMC) 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. Backward analyses can complement forward analyses, as backward analyses may be able to determine the reachability of error locations on programs where forward analyses may fail. An implementation of BBMC requires general support for backward analyses in CPAchecker, which is currently limited. We investigate the existing support for backward analyses in CPAchecker, and build on this to be able to implement the BBMC algorithm in CPAchecker. Moreover, we develop support for pointer aliasing in backward Predicate CPA, allowing backward analyses to be used on a larger set of programs and language features. An existing paper states that BBMC may be equivalent to k-induction. To test the comparative performance of the algorithms in practice, we evaluate the algorithms on a benchmark to see when they are indeed equivalent and in what cases they differ. Finally, we consider further work to be done and future improvements both for the BBMC algorithm and the support for backward analyses.