Формальная верификация программ, написанных на функционально-потоковом языке параллельного программирования
Аннотация
Работа посвящена доказательству корректности параллельных программ на основе аксиоматического подхода. Описана формальная система для функционально-потокового языка параллельного программирования Пифагор, в рамках которой можно проводить доказательства.
Об авторах
Мария Сергеевна Кропачева
Сибирский федеральный университет
Россия
аспирант
Россия
аспирант
Александр Иванович Легалов
Сибирский федеральный университет
Россия
профессор
Россия
профессор
Список литературы
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
Просмотров: 542
Послать статью по эл. почте 