In this thesis, we are concerned with the safety and security of programs. The problems addressed here are the correctness of SiJa (a subset of Java) source code and Java bytecode, and the information flow security of SiJa programs. A lot of research has been made on these topics, but almost all of them study each topic independently and no approach can handle all of these aspects. We propose a uniform framework that integrates the effort of proving correctness and security into one process. The core concept for this uniform approach is sound program transformation based on symbolic execution and deduction. The correctness of SiJa source code is verified with KeY, a symbolic execution based approach. Partial evaluation actions are interleaved during symbolic execution to reduce the proof size. By synthesizing the symbolic execution tree achieved in the source code verification phase, we can generate a program that is bisimilar to, but also more optimized than, the original one with respect to a set of observable locations. The soundness of program transformation is proven. Apply the sound program transformation approach, we can generate a program bisimilar to the original program with respect to the low security level variables. This results in a more precise analysis of information flow security than the approaches based on security type systems. We can also generate Java bytecode from SiJa source code program transformation approach, where the the correctness of the Java bytecode is guaranteed and compiler verification is not necessary.