Program verification has been one of the important issues in computer science since people started doing programming. It has been part of software engineering life cycle to guarantee the correctness of a program. Most of the time, an intensive testing is sufficient, however it is difficult (in some cases even impossible) to generate a complete test scenario. Therefore, in general, testing cannot completely discover all bugs. Program verification which is based on formal method is one of the alternatives to complement program testing. This idea of proving the correctness of a program based on mathematical proof was proposed in the late 60’s. Unfortunately, until now it can only be used in a specific task by a specific task force with special training. The difficulty of program verification lies on its complexity and deep detail. To be able to capture all possibilities, the formalization of the program has to be done in detail. The program needs to be modelled into some formula using what we call programming logic while the program may have highly abstracted data structures. The formalization becomes a lot more complicated than setting up a mathematical equation. The amount of work in doing program verification is usually a lot longer and a lot more difficult than developing the program itself. In this research, the focus is on providing expressive programming logic and the automation of it. The current state of the art of logic automation/mechanization has some flaws. The flaws were investigated during the experiment with simple programming languages called VSPL (Very Simple Programming Language) and SIL (Simple Imperative Language). A new method of logic mechanization which is called external embedding is proposed. Automation of the logic turns out to be quite difficult. As the underlying logic of HOL is not complete, it is some time impossible to ask the computer to do any logic reduction computation in finite time. Therefore, the system is allowed to have an interactive proving procedure in proving a program which may require human expertise. However, the main problem of complexity and deep detail remains. To reduce the complexity, a modular and compositional programming logic is proposed. The modularity allows us to see a complex problem as several simple problems which can be solved easily and independently. The composition allows us to combine the solutions of small problems as a solution to the original complex problem. This dissertation elaborates external embedding for logic mechanization which provides more features on doing verification of concrete programs. The associated programming logic is made modular and compositional by applying catamorphism concept as in functional programming. It yields some algebras of programming logic that can be composed independently. This approach is then applied to reactive systems which contain concurrency in an experimental programming language called SIP (Sequential Interleaved Processes). The concurrency formalism is based on UNITY. The proposed approach has been implemented in two prototype tools: xMech and LinguHOL. The xMech program verification tool is a prototype that can verify imperative programs and concurrent systems. The imperative language is quite simple, while the concurrent system language is a more concrete language than the UNITY language. The LinguHOL tool is another prototype which shows the extensibility of the concept and providing a library to replace the human expertise. It focuses on database applications where the formalism of SQL language is embedded.