Geodesic
Formal Verification of Programs in Functional Dataflow Parallel Language
Modelirovanie i analiz informacionnyh sistem, Tome 19 (2012) no. 5, pp. 81-99.

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

The article is devoted to the methods of proving parallel programs correctness that are based on the axiomatic approach. Formal system for functional data-flow parallel programming language Pifagor is described. On the basis of this system programs correctness could be proved.
Keywords: functional data-flow parallel programming, Pifagor programming language, programs formal verification. 
@article{MAIS_2012_19_5_a8,
     author = {M. S. Kropacheva and A. I. Legalov},
     title = {Formal {Verification} of {Programs} in {Functional} {Dataflow} {Parallel} {Language}},
     journal = {Modelirovanie i analiz informacionnyh sistem},
     pages = {81--99},
     publisher = {mathdoc},
     volume = {19},
     number = {5},
     year = {2012},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/MAIS_2012_19_5_a8/}
}
TY  - JOUR
AU  - M. S. Kropacheva
AU  - A. I. Legalov
TI  - Formal Verification of Programs in Functional Dataflow Parallel Language
JO  - Modelirovanie i analiz informacionnyh sistem
PY  - 2012
SP  - 81
EP  - 99
VL  - 19
IS  - 5
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/MAIS_2012_19_5_a8/
LA  - ru
ID  - MAIS_2012_19_5_a8
ER  - 
%0 Journal Article
%A M. S. Kropacheva
%A A. I. Legalov
%T Formal Verification of Programs in Functional Dataflow Parallel Language
%J Modelirovanie i analiz informacionnyh sistem
%D 2012
%P 81-99
%V 19
%N 5
%I mathdoc
%U http://geodesic.mathdoc.fr/item/MAIS_2012_19_5_a8/
%G ru
%F MAIS_2012_19_5_a8
M. S. Kropacheva; A. I. Legalov. Formal Verification of Programs in Functional Dataflow Parallel Language. Modelirovanie i analiz informacionnyh sistem, Tome 19 (2012) no. 5, pp. 81-99. http://geodesic.mathdoc.fr/item/MAIS_2012_19_5_a8/

[1] V. A. Nepomnyaschii, O. M. Ryakin, Prikladnye metody verifikatsii programm, Radio i svyaz, M., 1988, 255 pp.

[2] C. A. R. Hoare, “An axiomatic basis for computer programming”, Communications of the ACM, 10:12 (1969), 576–585 | DOI

[3] I. S. Anureev, I. V. Maryasov, V. A. Nepomnyaschii, “Verifikatsiya C-programm na osnove smeshannoi aksiomaticheskoi semantiki”, Modelirovanie i analiz informatsionnykh sistem, 17:3 (2010), 5–28

[4] A. I. Legalov, “Funktsionalnyi yazyk dlya sozdaniya arkhitekturno-nezavisimykh parallelnykh programm”, Vychislitelnye tekhnologii, 2005, no. 1(10), 71–89 | Zbl

[5] Yu. V. Udalova, A. I. Legalov, N. Yu. Sirotinina, “Metody otladki i verifikatsii funktsionalno-potokovykh parallelnykh programm”, Zhurnal Sibirskogo federalnogo universiteta. Seriya: Tekhnika i tekhnologii, 4:2 (2011), 213–224

[6] A. I. Legalov, F. A. Kazakov, D. A. Kuzmin, D. V. Privalikhin, Funktsionalnaya model parallelnykh vychislenii i yazyk programmirovaniya «Pifagor», http://www.softcraft.ru/fppp.shtml | Zbl

[7] A. I. Legalov, “Ispolzovanie asinkhronno postupayuschikh dannykh v potokovoi modeli vychislenii”, Tretya sibirskaya shkola-seminar po parallelnym vychisleniyam, Izd-vo Tomskogo un-ta, Tomsk, 2006, 113–120

[8] M. S. Kropacheva, “Formalizatsiya semantiki funktsionalno-potokovogo yazyka parallelnogo programmirovaniya Pifagor”, Problemy informatizatsii regiona, PIR-2011: Materialy XII Vserossiiskoi nauchno-prakticheskoi konferentsii, Sibirskii federalnyi universitet, Krasnoyarsk, 2011, 144–148

[9] L. Chen, Matematicheskaya logika i avtomaticheskoe dokazatelstvo teorem, ed. S. Yu. Maslov, Nauka, M., 1983, 358 pp. | MR | Zbl

[10] J. Harrison, Handbook Of Practical Logic And Automated Reasoning, Cambridge University Press, New York, 2009, 781 pp. | MR