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 条
  • [31] A dynamic logic for the formal verification of java card programs
    Universität Karlsruhe, Institut für Logik, Komplexität und Deduktionssysteme, Karlsruhe
    D-76128, Germany
    Lect. Notes Comput. Sci., 1600, (6-24):
  • [32] Formal verification of protocol properties of sequential java programs
    College of Computer Science and Technology, Jilin University, 2699 Qianjin Street, Changchun, 130012, China
    Proc Int Comput Software Appl Conf, (475-482):
  • [33] Formal verification of concurrent programs using the Larch prover
    Chetali, B
    IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 1998, 24 (01) : 46 - 62
  • [34] Formal Verification of Spacecraft Control Programs (Experience Report)
    Mokhov, Andrey
    Lukyanov, Georgy
    Lechner, Jakob
    PROCEEDINGS OF THE 12TH ACM SIGPLAN INTERNATIONAL SYMPOSIUM ON HASKELL (HASKELL '19), 2019, : 139 - 145
  • [35] Towards Formal Verification of State Continuity for Enclave Programs
    Jangid, Mohit Kumar
    Chen, Guoxing
    Zhang, Yinqian
    Lin, Zhiqiang
    PROCEEDINGS OF THE 30TH USENIX SECURITY SYMPOSIUM, 2021, : 573 - 590
  • [36] Formal Verification of the Race Condition Vulnerability in Ladder Programs
    Mesli-Kesraoui, Soraya
    Goubali, Olga
    Kesraoui, Djamal
    Eloumami, Ibtihal
    Oquendo, Flavio
    2020 IEEE CONFERENCE ON CONTROL TECHNOLOGY AND APPLICATIONS (CCTA), 2020, : 892 - 897
  • [37] Methods and Tools for Formal Verification of Cloud Sisal Programs
    Kasyanov, Victor N.
    Kasyanova, Elena, V
    2ND INTERNATIONAL CONFERENCE ON MATHEMATICS AND COMPUTERS IN SCIENCE AND ENGINEERING (MACISE 2020), 2020, : 219 - 222
  • [38] SYSTEMATIC TESTING AND FORMAL VERIFICATION TO VALIDATE REACTIVE PROGRAMS
    MULLERBURG, M
    HOLENDERSKI, L
    MAFFEIS, O
    MERCERON, A
    MORLEY, M
    SOFTWARE QUALITY JOURNAL, 1995, 4 (04) : 287 - 307
  • [39] Formal Verification of Ladder Logic programs using NuSMV
    Kottler, Sam
    Khayamy, Mehdy
    Hasan, Syed Rafay
    Elkeelany, Omar
    SOUTHEASTCON 2017, 2017,
  • [40] Formal Verification of Higher-Order Probabilistic Programs
    Sato, Tetsuya
    Aguirre, Alejandro
    Barthe, Gilles
    Gaboardi, Marco
    Garg, Deepak
    Hsu, Justin
    PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2019, 3 (POPL):
12345