Development of automated means for proving programs properties

A method for static program verification based on automated theorem proving is described. A function defined on the set of pairs of natural numbers lists is taken as a model for program. A function on the set of natural numbers is taken as a simplified model. The following security property is considered: only if the secret key is given to the input, the program may print the secret value to the output. The proofs for example programs are built with the Coq automated theorem prover. The common scheme for such proofs is derived and transformed into a Coq proving tactic. In conclusion, the ideas for the further researches are discussed.