Formal Verification of Programs in the Functional Data-flow Parallel Language

被引：4
|
作者：
Kropacheva, M. S. [1 ]
Legalov, A. I. [1 ]
机构：
[1] Siberian Fed Univ, Inst Space & Informat Technol, Krasnoyarsk, Russia
来源：
AUTOMATIC CONTROL AND COMPUTER SCIENCES | 2013年 / 47卷 / 07期
关键词：
functional data-flow parallel programming; Pifagor programming language; programs formal verification;
D O I：
10.3103/S0146411613070225
中图分类号：
TP [自动化技术、计算机技术];
学科分类号：
0812 ;
摘要：
The article is devoted to the methods of proving parallel programs correctness, that are based on the axiomatic approach. Formal system for functional data-flow parallel programming language Pifagor is described. On the basis of this system programs correctness could be proved.
引用
收藏
页码：373 / 384
页数：12
相关论文
共 50 条
  • [1] A REVIEW OF SPECIFICATION AND VERIFICATION METHODS FOR PARALLEL PROGRAMS, INCLUDING THE DATA-FLOW APPROACH
    DESHPANDE, AK
    KAVI, KM
    [J]. PROCEEDINGS OF THE IEEE, 1989, 77 (12) : 1816 - 1828
  • [2] Parallel data-flow analysis of explicitly parallel programs
    Knoop, J
    [J]. EURO-PAR'99: PARALLEL PROCESSING, 1999, 1685 : 391 - 400
  • [3] EDDA, A LANGUAGE BASED ON PETRINETS AND THE DATA-FLOW PRINCIPLE FOR THE DEVELOPMENT OF PARALLEL PROGRAMS
    KERNER, H
    RAINEL, H
    [J]. MICROPROCESSING AND MICROPROGRAMMING, 1986, 18 (1-5): : 299 - 305
  • [4] DATA-FLOW EQUATIONS FOR EXPLICITLY PARALLEL PROGRAMS
    GRUNWALD, D
    SRINIVASAN, H
    [J]. SIGPLAN NOTICES, 1993, 28 (07): : 159 - 168
  • [5] FORMAL VERIFICATION OF PARALLEL PROGRAMS
    KELLER, RM
    [J]. COMMUNICATIONS OF THE ACM, 1976, 19 (07) : 371 - 384
  • [6] CIVL: Formal Verification of Parallel Programs
    Zheng, Manchun
    Rogers, Michael S.
    Luo, Ziqing
    Dwyer, Matthew B.
    Siegel, Stephen F.
    [J]. 2015 30TH IEEE/ACM INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING (ASE), 2015, : 830 - 835
  • [7] Formal verification of synchronous data-flow program transformations toward certified compilers
    Van Chan NGO
    JeanPierre TALPIN
    Thierry GAUTIER
    Paul Le GUERNIC
    Lo c BESNARD
    [J]. Frontiers of Computer Science, 2013, 7 (05) : 598 - 616
  • [8] Formal verification of synchronous data-flow program transformations toward certified compilers
    Van Chan Ngo
    Jean-Pierre Talpin
    Thierry Gautier
    Paul Le Guernic
    Loïc Besnard
    [J]. Frontiers of Computer Science, 2013, 7 : 598 - 616
  • [9] A Symbolic Methodology for Formal Verification of High-level Data-Flow Synthesis
    Yang, Zhi
    Lv, Chao
    Ma, Guangsheng
    Shao, Jingbo
    [J]. 2008 9TH INTERNATIONAL CONFERENCE ON SOLID-STATE AND INTEGRATED-CIRCUIT TECHNOLOGY, VOLS 1-4, 2008, : 2345 - +
  • [10] Formal verification of synchronous data-flow program transformations toward certified compilers
    Van Chan Ngo
    Talpin, Jean-Pierre
    Gautier, Thierry
    Le Guernic, Paul
    Besnard, Loic
    [J]. FRONTIERS OF COMPUTER SCIENCE, 2013, 7 (05) : 598 - 616
12345