This thesis is devoted to automatic program verification. The problem is investigated in both theoretical and practical aspects. In the theoretical part we formulate a formal method which is based on a special three-valued calculus. We also prove theorems about properties of this formalism which are crucial for its practical applicability. In the practical part we describe a software implementation of the verification system based on the new formalism. We also present a solution to the most difficult problem every automatic verification system designer faces. This is the problem of constructing a proof procedure for the resulting formulae.
The original requirements imposed on the automatic verification system are as follows:
\(\bullet\) The system must verify programs from the largest subset of C.
\(\bullet\) The system must be simple to extend.
\(\bullet\) It must be possible to prove partial correctness of a program as well as the absence of dynamic errors during its computation.