Formal Verification of Programs in the Pifagor Language

Тип публикации: доклад, тезисы доклада, статья из сборника материалов конференций

Конференция: International Conference on Parallel Computing Technologies (PaCT); St Petersburg, RUSSIA; St Petersburg, RUSSIA

Год издания: 2013

Идентификатор DOI: 10.1007/978-3-642-39958-9-7

Ключевые слова: Functional data-flow parallel programming, Pifagor programming language, programs formal verification, Axiomatic system, Dataflow, Formal verifications, Parallel program, Recursions, Support programs, Computer programming languages, Functional programming, Parallel architectures, Parallel programming

Аннотация: 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.

Ссылки на полный текст

Издание

Журнал: PARALLEL COMPUTING TECHNOLOGIES (PACT 2013)

Выпуск журнала: Vol. 7979

Номера страниц: 80-89

ISSN журнала: 03029743

Место издания: BERLIN

Издатель: SPRINGER-VERLAG BERLIN

Авторы

  • Kropacheva Mariya (Siberian Fed Univ, Inst Space & Informat Technol, Krasnoyarsk 660074, Russia)
  • Legalov Alexander (Siberian Fed Univ, Inst Space & Informat Technol, Krasnoyarsk 660074, Russia)

Вхождение в базы данных

Информация о публикациях загружается с сайта службы поддержки публикационной активности СФУ. Сообщите, если заметили неточности.

Вы можете отметить интересные фрагменты текста, которые будут доступны по уникальной ссылке в адресной строке браузера.