Geodesic
Automation of formal verification of programs in the Pifagor language
Modelirovanie i analiz informacionnyh sistem, Tome 22 (2015) no. 4, pp. 578-589

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

Nowadays, due to software sophistication, programs correctness is more often proved by means of formal verification. The method of deduction based on Hoare logic could be used for any programming language and it has the capability of partial automation of the proof process. However, the method of deduction is not widely used for verification of parallel programs because of high complexity of the process. The usage of the functional data-flow paradigm of parallel programming allows to decrease the complexity of the proof process. In this article a proof process of correctness of functional data-flow parallel programs in the Pifagor language is considered. The proof process of a program correctness is considered as a tree where each node is a program data-flow graph, whose edges are marked with formulas in a specification language. The tree root is the initial program data-flow graph with a precondition and a postcondition, which describe restrictions on input variables and correctness conditions of the result of the program execution, respectively. Basic transformations of the data-flow graph are edge marking, equivalent transformation, splitting, folding of the program. By means of these transformations the data-flow graph is transformed and finally is reduced to a set of formulas in the specification language. If all these formulas are identically true, the program is correct. Several modules is distinguished in the system: “Program correctness prover”, “Axioms and theorems library management system” and “Errors analysis and output of information about errors”. According to this architecture, the toolkit for supporting formal verification was developed. The main functionality of the system implementation is considered.
Keywords: functional data-flow parallel programming, Pifagor programming language, programs formal verification, toolkit for supporting formal verification. 
@article{MAIS_2015_22_4_a9,
     author = {M. S. Ushakova and A. I. Legalov},
     title = {Automation of formal verification of programs in the {Pifagor} language},
     journal = {Modelirovanie i analiz informacionnyh sistem},
     pages = {578--589},
     publisher = {mathdoc},
     volume = {22},
     number = {4},
     year = {2015},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/MAIS_2015_22_4_a9/}
}
TY  - JOUR
AU  - M. S. Ushakova
AU  - A. I. Legalov
TI  - Automation of formal verification of programs in the Pifagor language
JO  - Modelirovanie i analiz informacionnyh sistem
PY  - 2015
SP  - 578
EP  - 589
VL  - 22
IS  - 4
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/MAIS_2015_22_4_a9/
LA  - en
ID  - MAIS_2015_22_4_a9
ER  - 
%0 Journal Article
%A M. S. Ushakova
%A A. I. Legalov
%T Automation of formal verification of programs in the Pifagor language
%J Modelirovanie i analiz informacionnyh sistem
%D 2015
%P 578-589
%V 22
%N 4
%I mathdoc
%U http://geodesic.mathdoc.fr/item/MAIS_2015_22_4_a9/
%G en
%F MAIS_2015_22_4_a9
M. S. Ushakova; A. I. Legalov. Automation of formal verification of programs in the Pifagor language. Modelirovanie i analiz informacionnyh sistem, Tome 22 (2015) no. 4, pp. 578-589. http://geodesic.mathdoc.fr/item/MAIS_2015_22_4_a9/