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 条
  • [21] Towards verification of C programs. C-light language and its formal semantics
    Nepomniaschy, VA
    Anureev, IS
    Mikhailov, IN
    Promskii, AV
    PROGRAMMING AND COMPUTER SOFTWARE, 2002, 28 (06) : 314 - 323
  • [22] FORMAL VERIFICATION OF A CLASS OF CONCURRENT PROGRAMS.
    Mori, Masaaki
    Taniguchi, Kenichi
    Kasami, Tadao
    Fujii, Mamoru
    Systems, computers, controls, 1981, 10 (04): : 11 - 20
  • [23] A formal framework for synthesis and verification of logic programs
    Avellone, A
    Ferrari, M
    Fiorentini, C
    LOGIC BASED PROGRAM SYNTHESIS AND TRANSFORMATION, 2001, 2042 : 1 - 17
  • [24] EXTRACTION AND VERIFICATION OF PROGRAMS BY ANALYSIS OF FORMAL PROOFS
    ALEXI, W
    THEORETICAL COMPUTER SCIENCE, 1988, 61 (2-3) : 225 - 258
  • [25] Formal Verification of UML Statecharts using the LOTOS Formal Language
    Javani, Mohamad
    Neysiani, Behzad Soleimani
    Babamir, Seyed Morteza
    2015 2ND INTERNATIONAL CONFERENCE ON KNOWLEDGE-BASED ENGINEERING AND INNOVATION (KBEI), 2015, : 754 - 760
  • [26] Loop-invariant Optimization in the Pifagor Language
    Vasilev, V. S.
    Legalov, A. I.
    AUTOMATIC CONTROL AND COMPUTER SCIENCES, 2018, 52 (07) : 843 - 849
  • [27] Three Early Formal Approaches to the Verification of Concurrent Programs
    Jones, Cliff B.
    MINDS AND MACHINES, 2024, 34 (SUPPL 1) : 73 - 92
  • [28] Formal verification of secure programs in the presence of side effects
    Black, PE
    Windley, PJ
    PROCEEDINGS OF THE THIRTY-FIRST HAWAII INTERNATIONAL CONFERENCE ON SYSTEM SCIENCES, VOL III: EMERGING TECHNOLOGIES TRACK, 1998, : 327 - 334
  • [29] Formal Verification of Quantum Programs: Theory, Tools, and Challenges
    Lewis, Marco
    Soudjani, Sadegh
    Zuliani, Paolo
    ACM TRANSACTIONS ON QUANTUM COMPUTING, 2024, 5 (01):
  • [30] Formal Specification-Based Inspection for Verification of Programs
    Liu, Shaoying
    Chen, Yuting
    Nagoya, Fumiko
    McDermid, John A.
    IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 2012, 38 (05) : 1100 - 1122
12345