Рассмотрена математическая модель параллельного алгоритма, и дано математическое описание проблемы анализа параллельного алгоритма, которое заключается в построении формального доказательства соответствия алгоритма своей спецификации. Изложены методы анализа параллельных алгоритмов в рамках представленной модели, являющиеся обобщением методов анализа блок-схем последовательных программ путём построения индуктивных утверждений.

1. R. W. Floyd, "Assigning meanings to programs", Proc. Symp. Appl. Math., 19; in: J.T.Schwartz (ed.), Mathematical Aspects of Computer Science, pp. 19-32, American Mathematical Society, Providence, R.I., 1967.

2. R. Milner, "A Calculus of Communicating Systems", Lecture Notes in Computer Science, vol. 92, Springer, 1980.

3. Z. Manna, "Mathematical theory of computation", McGraw-Hill, 1974.

4. N. Francez, "Verification of programs", Addison-Wesley Publishers Ltd., 1992.

5. Р. Андерсон, "Доказательство правильности программ", М.: Мир, 1982.

6. Jacques Loeckx, and Kurt Sieber, "The Foundations of Program Verification", Wiley - Teubner, Stuttgart, 1984.

7. В. А. Непомнящий, О. М. Рякин, "Прикладные методы верификации программ", М.: Радио и связь, 1988.

8. С. А. Абрамов, "Элементы анализа программ. Частичные функции на множестве состояний", М.: Наука, 1986.