Послать статью по эл. почте 
Формальная верификация программ, написанных на функционально-потоковом языке параллельного программирования
https://doi.org/10.18255/1818-1015-2012-5-81-99
Аннотация
Работа посвящена доказательству корректности параллельных программ на основе аксиоматического подхода. Описана формальная система для функционально-потокового языка параллельного программирования Пифагор, в рамках которой можно проводить доказательства.
Об авторах
Мария Сергеевна КропачеваРоссия
аспирант
Александр Иванович Легалов
Россия
профессор
Список литературы
1. Непомнящий В.А., Рякин О.М. Прикладные методы верификации программ. М.: Радио и связь, 1988. 255 с.
2. Hoare C. A. R. An axiomatic basis for computer programming // Communications of the ACM. 1969. Vol. 10. N. 12. P. 576–585.
3. Ануреев И. С., Марьясов И. В., Непомнящий В. А. Верификация C-программ на основе смешанной аксиоматической семантики // Моделирование и анализ информационных систем. 2010. Т. 17, № 3. C. 5–28.
4. Легалов А.И. Функциональный язык для создания архитектурно-независимых параллельных программ // Вычислительные технологии. 2005. № 1 (10). С. 71–89.
5. Удалова Ю.В., Легалов А.И., Сиротинина Н.Ю. Методы отладки и верификации функционально-потоковых параллельных программ // Журнал Сибирского федерального университета. Серия: Техника и технологии. 2011. Т. 4. № 2. С. 213–224.
6. Легалов А.И., Казаков Ф.А., Кузьмин Д.А., Привалихин Д.В. Функциональная модель параллельных вычислений и язык программирования «Пифагор»: ttp://www.softcraft.ru/fppp.shtml
7. Легалов А.И. Использование асинхронно поступающих данных в потоковой модели вычислений / Третья сибирская школа-семинар по параллельным вычислениям. Томск: Изд-во Томского ун-та, 2006. С. 113–120.
8. Кропачева М.С. Формализация семантики функционально-потокового языка параллельного программирования Пифагор // Проблемы информатизации региона. ПИР-2011: Материалы XII Всероссийской научно-практической конференции. Красноярск: Сибирский федеральный университет. 2011. С. 144–148.
9. Чень Л. Математическая логика и автоматическое доказательство теорем / Под ред. С.Ю. Маслова. М.: Наука, 1983. 358 с.
10. Harrison J. Handbook Of Practical Logic And Automated Reasoning New York: Cambridge University Press, 2009. 781 p.
Дополнительные файлы
Для цитирования: Кропачева М.С., Легалов А.И. Формальная верификация программ, написанных на функционально-потоковом языке параллельного программирования. Моделирование и анализ информационных систем. 2012;19(5):81-99. https://doi.org/10.18255/1818-1015-2012-5-81-99
For citation: Kropacheva M.S., Legalov A.I. Formal Verification of Programs in Functional Dataflow Parallel Language. Modeling and Analysis of Information Systems. 2012;19(5):81-99. (In Russ.) https://doi.org/10.18255/1818-1015-2012-5-81-99
Обратные ссылки
- Обратные ссылки не определены.
