Formal validation of data-parallel programs: a two-component assertional proof system for a simple language

被引：4
|
作者：
Bouge, L
Cachera, D
LeGuyadec, Y
Utard, G
Virot, B
机构：
[1] UNIV ORLEANS,LIFO,F-45067 ORLEANS 2,FRANCE
[2] VALORIA,VANNES,FRANCE
来源：
THEORETICAL COMPUTER SCIENCE | 1997年 / 189卷 / 1-2期
关键词：
D O I：
10.1016/S0304-3975(97)00041-8
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
We present a proof system for a simple data-parallel kernel language called L. This proof system is based on a two-component assertion language. We define a weakest preconditions calculus and analyze its definability properties. This calculus is used to prove the completeness of the proof system. We also present a two-phase proof methodology, yielding proofs similar to those for scalar languages. We finally discuss other approaches.
引用
收藏
页码：71 / 107
页数：37
相关论文
共 44 条
  • [1] A PROOF SYSTEM FOR A SIMPLE DATA-PARALLEL PROGRAMMING LANGUAGE
    BOUGE, L
    LEGUYADEC, Y
    UTARD, G
    VIROT, B
    APPLICATIONS IN PARALLEL AND DISTRIBUTED COMPUTING, 1994, 44 : 63 - 72
  • [2] Loosely synchronized execution model for a simple data-parallel language
    Lect Notes Comput Sci, (732):
  • [3] 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
  • [4] On the inspection policy of a two-component parallel system with failure interaction
    Zequeira, RI
    Bérenguer, C
    RELIABILITY ENGINEERING & SYSTEM SAFETY, 2005, 88 (01) : 99 - 107
  • [5] Efficient index generation for compiling two-level mappings in data-parallel programs
    Shih, KP
    Sheu, JP
    Huang, CH
    Chang, CY
    JOURNAL OF PARALLEL AND DISTRIBUTED COMPUTING, 2000, 60 (02) : 189 - 216
  • [6] Inspection optimal model of a two-component parallel system with failure dependence
    Cai Jing
    Zuo Hongfu
    Wang Huawei
    PROCEEDINGS OF THE FIRST INTERNATIONAL CONFERENCE ON MAINTENANCE ENGINEERING, 2006, : 345 - 351
  • [7] Optimal Replacement Policies for Two-component Parallel System with Stochastic Dependence
    Malki, Zouheir
    Ait-Kadi, Daoud
    Ouali, Mohamed-Salah
    PROCEEDINGS OF 2013 INTERNATIONAL CONFERENCE ON INDUSTRIAL ENGINEERING AND SYSTEMS MANAGEMENT (IEEE-IESM 2013), 2013, : 341 - 345
  • [8] Maintenance cost analysis of a two-component parallel system with failure interaction
    Zequeira, RI
    Bérenguer, C
    ANNUAL RELIABILITY AND MAINTAINABILITY SYMPOSIUM, 2004 PROCEEDINGS, 2004, : 220 - 225
  • [9] The complexity of the 'simple' two-component system KdpD/KdpE in Escherichia coli
    Heermann, Ralf
    Jung, Kirsten
    FEMS MICROBIOLOGY LETTERS, 2010, 304 (02) : 97 - 106
  • [10] A Delay-Time-Based Inspection Model for A Two-Component Parallel System
    Wang, Wenbin
    Liu, Xuejuan
    Peng, Rui
    Guo, Li
    PROCEEDINGS OF 2013 INTERNATIONAL CONFERENCE ON QUALITY, RELIABILITY, RISK, MAINTENANCE, AND SAFETY ENGINEERING (QR2MSE), VOLS I-IV, 2013, : 616 - 619
12345