Reverse Program Synthesis for Backward Reachability Analysis in CPAchecker

CPAchecker now supports reachability analysis, which can search for a path from the initial program location to the error location. This project is a Proof of Concept, to implement the Backward Reachability Analysis, i.e. search for a path from the error location to the initial location. The main goal of this project is to implement a control-flow automata (CFA) transformer in CPAchecker that reverses program executions by following the transitions backward, such that for any program path in the original CFA, there is a corresponding equisatisfiable path in reverse CFA. After the transformation, the existing analysis can be applied to verify the reverse CFA, thus enabling the Backward Reachability Analysis.