This thesis describes the implementation of a tool chain which allows the analysis of C control programs for the purpose of program understanding and model abstraction. Relying in dierent analysis methods, the tool chain allows analyzing program code and creating dierent abstract model representations, such as an abstract syntax tree, value sets and a control ow graph. For acquiring those basic model representations, the Frama-C analysis framework has been used. Further, those models are then used to perform a symbolic execution of the program, which identies all paths of the program and retrieves the conditions for each path. The theorem prover Z3 is used to determine the solvability of the paths. By performing the symbolic execution multiple times, a state model of the program can be created. The analysis results, in particular, the created model representations and the state model, can nally help developers in analyzing and understanding the behavior of complex control programs.