Omnipresence of computer systems in modern technological applications makes the question of their reliability essential. In this thesis, we investigate equational logic as a foundation for the verification of programs written in an imperative language. Our approach aims at automating the verification of program properties while offering a formalism suited to software developers for reasoning about programs. Precisely, our work addresses the automatic translation of imperative programs into equational logic in order to verify their correctness. We studied two classes of programs. In the first class, assignment is the sole language statement with side effect. We developed an algorithm to translate the programs in this class into a set of equations. This algorithm is expressed as a rewrite system defining the language's semantics. We showed, with a theorem prover, the convergence of our rewrite system. The second class is defined by adding to the programming language call-by-reference parameter passing mode and mutable lists. These mechanisms introduce the ability of handling aliases in programs. We define restrictions on the use of aliases which allow us to propose an algorithm for the translation into equations of the programs in the new class. The equational definition we obtain does not involve an explicit model of the program's memory. The equations produced by the translation of a program can then be used in proof systems in order to verify properties of the program. The properties are also expressed as equations. We validate our approach by implementing the translation algorithms and by proving interesting program properties from the equations produced by our method.
