Abstract
The article is devoted to the methods of proving parallel programs correctness, that are based on the Hoare axiomatic system. In this article such system is being developed for proving the correctness of the programs in the functional data-flow parallel programming language Pifagor. Recursion correctness is proved by induction. This method could be used as a base of a toolkit to support program correctness proving, since it could be made automate at many stages.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Nepomnyashiy, V.A., Ryakin, O.M.: Applied Methods for Programs Verification. Radio i svyaz, Moscow (1988)
Hoare, C.A.R.: An Axiomatic Basis for Computer Programming. CACM 10(12), 576–585 (1969)
Anureev, I.S., Maryasov, I.V., Nepomniaschy, V.A.: The Mixed Axiomatic Semantics Method for C-program Verification. MAIS 17(3), 5–28 (2010)
Udalova, U.V., Legalov, A.I., Sirotinina, N.U.: Debug and Verification of Function-Stream Parallel Programs. Journal of Siberian Federal University. Engineering and Technologies 4(2), 213–224 (2011)
Legalov, A.I.: The Functional Programming Language for Creating Architecture-Independent parallel Programs. Computational Technologies 10(1), 71–89 (2005)
Kropacheva, M.S.: Formalization of the Semantics for the Functional Data-Flow Parallel Language Pifagor. In: 12th Russian Scientific-Practical Conference “The Problems of Region Informatization”, pp. 144–148. Siberian Federal University, Krasnoyarsk (2011)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kropacheva, M., Legalov, A. (2013). Formal Verification of Programs in the Pifagor Language. In: Malyshkin, V. (eds) Parallel Computing Technologies. PaCT 2013. Lecture Notes in Computer Science, vol 7979. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-39958-9_7
Download citation
DOI: https://doi.org/10.1007/978-3-642-39958-9_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-39957-2
Online ISBN: 978-3-642-39958-9
eBook Packages: Computer ScienceComputer Science (R0)