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 条
  • [41] Three Early Formal Approaches to the Verification of Concurrent Programs
    Cliff B. Jones
    Minds and Machines, 2024, 34 : 73 - 92
  • [42] Using Krakatoa for Teaching Formal Verification of Java Programs
    Divasón, Jose
    Romero, Ana
    Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2019, 11758 LNCS : 37 - 51
  • [43] A formal pattern language for refactoring of Lisp programs
    Leitao, AM
    SIXTH EUROPEAN CONFERENCE ON SOFTWARE MAINTENANCE AND REENGINEERING, PROCEEDINGS, 2002, : 186 - 192
  • [44] Formal Verification of Numerical Programs: From C Annotated Programs to Mechanical Proofs
    Boldo, Sylvie
    Marche, Claude
    MATHEMATICS IN COMPUTER SCIENCE, 2011, 5 (04) : 377 - 393
  • [45] Experimental Evaluation of a Planning Language Suitable for Formal Verification
    Siminiceanu, Radu I.
    Butler, Rick W.
    Munoz, Cesar A.
    MODEL CHECKING AND ARTIFICIAL INTELLIGENCE, 2009, 5348 : 132 - +
  • [46] Formal verification of a programming logic for a distributed programming language
    Zhang, C
    Olsson, RA
    Levitt, KN
    THEORETICAL COMPUTER SCIENCE, 1999, 216 (1-2) : 213 - 235
  • [47] VERIFICATION OF FILE MANIPULATION PROGRAMS IN THE LANGUAGE PASCAL
    NEPOMNYASHCHII, VA
    PROGRAMMING AND COMPUTER SOFTWARE, 1981, 7 (02) : 91 - 98
  • [48] Formal Verification of Language-Based Concurrent Noninterference
    Popescu, Andrei
    Hoezi, Johannes
    Nipkow, Tobias
    JOURNAL OF FORMALIZED REASONING, 2013, 6 (01): : 1 - 30
  • [49] Formal verification of C language based VLSI designs
    Fujita, M
    17TH INTERNATIONAL CONFERENCE ON VLSI DESIGN, PROCEEDINGS: DESIGN METHODOLOGIES FOR THE GIGASCALE ERA, 2004, : 93 - 100
  • [50] A Constrained ECA Language Supporting Formal Verification of WSNs
    Corradini, Flavio
    Culmone, Rosario
    Mostarda, Leonardo
    Tesei, Luca
    Raimondi, Franco
    2015 IEEE 29TH INTERNATIONAL CONFERENCE ON ADVANCED INFORMATION NETWORKING AND APPLICATIONS WORKSHOPS WAINA 2015, 2015, : 187 - 192
12345