Formal Verification of Programs in the Pifagor Language

被引：0
|
作者：
Kropacheva, Mariya [1 ]
Legalov, Alexander [1 ]
机构：
[1] Siberian Fed Univ, Inst Space & Informat Technol, Krasnoyarsk 660074, Russia
来源：
PARALLEL COMPUTING TECHNOLOGIES (PACT 2013) | 2013年 / 7979卷
关键词：
Functional data-flow parallel programming; Pifagor programming language; programs formal verification;
D O I：
暂无
中图分类号：
TP [自动化技术、计算机技术];
学科分类号：
0812 ;
摘要：
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.
引用
收藏
页码：80 / 89
页数：10
相关论文
共 50 条
  • [1] Verification of Programs with Mutual Recursion in Pifagor Language
    Ushakova, M. S.
    Legalov, A. I.
    AUTOMATIC CONTROL AND COMPUTER SCIENCES, 2018, 52 (07) : 850 - 866
  • [2] Formal Verification of Programs in the Functional Data-flow Parallel Language
    Kropacheva, M. S.
    Legalov, A. I.
    AUTOMATIC CONTROL AND COMPUTER SCIENCES, 2013, 47 (07) : 373 - 384
  • [3] Formal verification of PLC programs
    Rausch, M
    Krogh, BH
    PROCEEDINGS OF THE 1998 AMERICAN CONTROL CONFERENCE, VOLS 1-6, 1998, : 234 - 238
  • [4] FORMAL VERIFICATION OF PARALLEL PROGRAMS
    KELLER, RM
    COMMUNICATIONS OF THE ACM, 1976, 19 (07) : 371 - 384
  • [5] FORMAL VERIFICATION OF ADA PROGRAMS
    GUASPARI, D
    MARCEAU, C
    POLAK, W
    IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 1990, 16 (09) : 1058 - 1075
  • [6] CIVL: Formal Verification of Parallel Programs
    Zheng, Manchun
    Rogers, Michael S.
    Luo, Ziqing
    Dwyer, Matthew B.
    Siegel, Stephen F.
    2015 30TH IEEE/ACM INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING (ASE), 2015, : 830 - 835
  • [7] Formal Verification of Practical MPI Programs
    Vo, Anh
    Vakkalanka, Sarvani
    DeLisi, Michael
    Gopalakrishnan, Ganesh
    Kirby, Robert M.
    Thakur, Rajeev
    ACM SIGPLAN NOTICES, 2009, 44 (04) : 261 - 269
  • [8] Formal Verification of Spacecraft Control Programs
    Lukyanov, Georgy
    Mokhov, Andrey
    Lechner, Jakob
    ACM TRANSACTIONS ON EMBEDDED COMPUTING SYSTEMS, 2020, 19 (05)
  • [9] A Logic for Formal Verification of Quantum Programs
    Kakutani, Yoshihiko
    ADVANCES IN COMPUTER SCIENCE - ASIAN 2009: INFORMATION SECURITY AND PRIVACY, PROCEEDINGS, 2009, 5913 : 79 - 93
  • [10] Formal Verification of Signalling Programs with SafeCap
    Iliasov, Alexei
    Taylor, Dominic
    Laibinis, Linas
    Romanovsky, Alexander
    COMPUTER SAFETY, RELIABILITY, AND SECURITY (SAFECOMP 2018), 2018, 11093 : 91 - 106
12345