Formal Verification of Concurrency in Go

被引：0
|
作者：
Prasertsang, Anuchit [1 ]
Pradubsuwun, Denduang [1 ]
机构：
[1] Thammasat Univ, Fac Sci & Technol, Dept Comp Sci, Khet Phra Nakhon, Krung Thep Maha, Thailand
来源：
2016 13TH INTERNATIONAL JOINT CONFERENCE ON COMPUTER SCIENCE AND SOFTWARE ENGINEERING (JCSSE) | 2016年
关键词：
Go programming language (Go); CSP; FDR;
D O I：
暂无
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
Go is a programming language which is mainly designed for the concurrent programming. It supports concurrency derived from Hoare's Communicating Sequential Processes (CSP). Since a go-routine introduced by Go allows us to execute program simultaneously, a program behavior is asynchronous. It likely causes a failure. Hence, a formal verification is needed to assure the correctness of the program. In this paper, we have proposed a method to verify a program implemented by Go. A refinement checker for CSP or Failures Divergence Refinement (FDR) in [1] is used as a verification tool. We also give some experimental results to show effectiveness of our method.
引用
收藏
页码：258 / 261
页数：4
相关论文
共 50 条
  • [1] Formal Verification of Smart Contracts from the Perspective of Concurrency
    Qu, Meixun
    Huang, Xin
    Chen, Xu
    Wang, Yi
    Ma, Xiaofeng
    Liu, Dawei
    SMART BLOCKCHAIN, 2018, 11373 : 32 - 43
  • [2] Formal verification of an optimistic concurrency control algorithm using SPIN
    Makni, Achraf
    Bouaziz, Rafik
    Gargouri, Faiez
    TIME 2006: THIRTEENTH INTERNATIONAL SYMPOSIUM ON TEMPORAL REPRESENTATION AND REASONING, PROCEEDINGS, 2006, : 160 - +
  • [3] How Formal Dynamic Verification Tools Facilitate Novel Concurrency Visualizations
    Aananthakrishnan, Sriram
    DeLisi, Michael
    Vakkalanka, Sarvani
    Vo, Anh
    Gopalakrishnan, Ganesh
    Kirby, Robert M.
    Thakur, Rajeev
    RECENT ADVANCES IN PARALLEL VIRTUAL MACHINE AND MESSAGE PASSING INTERFACE, PROCEEDINGS, 2009, 5759 : 261 - +
  • [4] Formal verification of an access concurrency control algorithm for transaction time relations
    Makni, Achraf
    Bouaziz, Rafik
    Gargouri, Faiez
    ICEIS 2006: PROCEEDINGS OF THE EIGHTH INTERNATIONAL CONFERENCE ON ENTERPRISE INFORMATIONAL SYSTEMS: DATABASES AND INFORMATION SYSTEMS INTEGRATION, 2006, : 269 - +
  • [5] Bounded verification of message-passing concurrency in Go using Promela and Spin
    Dilley, Nicolas
    Lange, Julien
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2020, (314): : 34 - 45
  • [6] Formal Verification of UML MARTE Specifications Based on a True Concurrency Real Time Model
    Chabbat N.
    Saidouni D.E.
    Boukharrou R.
    Ghanemi S.
    Computing and Informatics, 2021, 39 (05) : 1022 - 1060
  • [7] FORMAL VERIFICATION OF UML MARTE SPECIFICATIONS BASED ON A TRUE CONCURRENCY REAL TIME MODEL
    Chabbat, Nadia
    Saidouni, Djamel Eddine
    Boukharrou, Radja
    Ghanemi, Salim
    COMPUTING AND INFORMATICS, 2020, 39 (05) : 1022 - 1060
  • [8] Threads as Resource for Concurrency Verification
    Duy-Khanh Le
    Chin, Wei-Ngan
    Teo, Yong Meng
    PROCEEDINGS OF THE 2015 ACM SIGPLAN WORKSHOP ON PARTIAL EVALUATION AND PROGRAM MANIPULATION (PEPM'15), 2015, : 73 - 84
  • [9] Simulation Refinement for Concurrency Verification
    Hesselink, Wim H.
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2008, 214 : 3 - 23
  • [10] Simulation refinement for concurrency verification
    Hesselink, Wim H.
    SCIENCE OF COMPUTER PROGRAMMING, 2011, 76 (09) : 739 - 755
12345