Geodesic
Development of automated means for proving programs properties
Prikladnaya Diskretnaya Matematika. Supplement, no. 7 (2014), pp. 148-150.

Voir la notice de l'article provenant de la source Math-Net.Ru

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.
Keywords: verification of programs, automated proof
Mots-clés : Coq. 
@article{PDMA_2014_7_a63,
     author = {A. O. Zhukovskaya and D. A. Stefantsov},
     title = {Development of automated means for proving programs properties},
     journal = {Prikladnaya Diskretnaya Matematika. Supplement},
     pages = {148--150},
     publisher = {mathdoc},
     number = {7},
     year = {2014},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/PDMA_2014_7_a63/}
}
TY  - JOUR
AU  - A. O. Zhukovskaya
AU  - D. A. Stefantsov
TI  - Development of automated means for proving programs properties
JO  - Prikladnaya Diskretnaya Matematika. Supplement
PY  - 2014
SP  - 148
EP  - 150
IS  - 7
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/PDMA_2014_7_a63/
LA  - ru
ID  - PDMA_2014_7_a63
ER  - 
%0 Journal Article
%A A. O. Zhukovskaya
%A D. A. Stefantsov
%T Development of automated means for proving programs properties
%J Prikladnaya Diskretnaya Matematika. Supplement
%D 2014
%P 148-150
%N 7
%I mathdoc
%U http://geodesic.mathdoc.fr/item/PDMA_2014_7_a63/
%G ru
%F PDMA_2014_7_a63
A. O. Zhukovskaya; D. A. Stefantsov. Development of automated means for proving programs properties. Prikladnaya Diskretnaya Matematika. Supplement, no. 7 (2014), pp. 148-150. http://geodesic.mathdoc.fr/item/PDMA_2014_7_a63/

[1] Hoare T., “The verifying compiler: a grand challenge for computing research”, J. ACM, 50:1 (2003), 63–69 | DOI

[2] Vereschagin N. K., Shen A., Lektsii po matematicheskoi logike i teorii algoritmov. Ch. 3. Vychislimye funktsii, 4-e izd., ispr., MTsNMO, M., 2012

[3] http://coq.inria.fr/

[4] Barendregt X., Lambda-ischislenie. Ego sintaksis i semantika, Mir, M., 1985 | MR | Zbl

[5] Pirs B., Tipy v yazykakh programmirovaniya, Lyambda press Dobrosvet, M., 2011