Geodesic
A toolkit for supporting formal verification of programs in the functional data-flow parallel programming language
Vestnik Ûžno-Uralʹskogo gosudarstvennogo universiteta. Seriâ Vyčislitelʹnaâ matematika i informatika, Tome 4 (2015) no. 2, pp. 58-70

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

The article is devoted to the architecture development of the toolkit for supporting formal verification of functional data-flow parallel programs in the Pifagor Language. The method ofdeduction based on Hoare logic is used for formal verification. A proof process is considered asa tree where each node is a program data-flow graph, whose edges are marked with formulasin a specification language. The tree root is the initial Hoare triple, namely the program data-flow graph with a precondition and a postcondition. In this article basic transformations of thedata-flow graph are considered: edge marking, equivalent transformation, splitting, folding of theprogram. By means of these transformations the initial triple is being transformed and finally isreduced to a set of formulas in the specification language. If all of these formulas are identicallytrue, then the program is correct. Architecture of the toolkit for supporting formal verification offunctional data-flow parallel programs is proposed, which allows to construct a proof three. Theimplementation of the toolkit is introduced and its main functionality is considered.
Keywords: functional data-flow parallel programming, Pifagor programming language, programs formal verification, toolkit for supporting formal verification. 
@article{VYURV_2015_4_2_a4,
     author = {M. S. Ushakova and A. I. Legalov},
     title = {A toolkit for supporting formal verification of programs in the functional data-flow parallel programming language},
     journal = {Vestnik \^U\v{z}no-Uralʹskogo gosudarstvennogo universiteta. Seri\^a Vy\v{c}islitelʹna\^a matematika i informatika},
     pages = {58--70},
     publisher = {mathdoc},
     volume = {4},
     number = {2},
     year = {2015},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/VYURV_2015_4_2_a4/}
}
TY  - JOUR
AU  - M. S. Ushakova
AU  - A. I. Legalov
TI  - A toolkit for supporting formal verification of programs in the functional data-flow parallel programming language
JO  - Vestnik Ûžno-Uralʹskogo gosudarstvennogo universiteta. Seriâ Vyčislitelʹnaâ matematika i informatika
PY  - 2015
SP  - 58
EP  - 70
VL  - 4
IS  - 2
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/VYURV_2015_4_2_a4/
LA  - ru
ID  - VYURV_2015_4_2_a4
ER  - 
%0 Journal Article
%A M. S. Ushakova
%A A. I. Legalov
%T A toolkit for supporting formal verification of programs in the functional data-flow parallel programming language
%J Vestnik Ûžno-Uralʹskogo gosudarstvennogo universiteta. Seriâ Vyčislitelʹnaâ matematika i informatika
%D 2015
%P 58-70
%V 4
%N 2
%I mathdoc
%U http://geodesic.mathdoc.fr/item/VYURV_2015_4_2_a4/
%G ru
%F VYURV_2015_4_2_a4
M. S. Ushakova; A. I. Legalov. A toolkit for supporting formal verification of programs in the functional data-flow parallel programming language. Vestnik Ûžno-Uralʹskogo gosudarstvennogo universiteta. Seriâ Vyčislitelʹnaâ matematika i informatika, Tome 4 (2015) no. 2, pp. 58-70. http://geodesic.mathdoc.fr/item/VYURV_2015_4_2_a4/