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 条
  • [21] FORMAL ASPECTS OF SERIALIZABILITY IN DATABASE CONCURRENCY CONTROL
    BERNSTEIN, PA
    SHIPMAN, DW
    WONG, WS
    IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 1979, 5 (03) : 203 - 216
  • [22] Formal Modeling for UML/MARTE Concurrency Resources
    Penil, Pablo
    Posadas, Hector
    Villar, Eugenio
    2010 15TH IEEE INTERNATIONAL CONFERENCE ON ENGINEERING OF COMPLEX COMPUTER SYSTEMS (ICECCS 2010), 2010, : 343 - 348
  • [23] Armed Cats: Formal Concurrency Modelling at Arm
    Alglave, Jade
    Deacon, Will
    Grisenthwaite, Richard
    Hacquard, Antoine
    Maranget, Luc
    ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2021, 43 (02):
  • [24] Concurrency in Go and Java']Java: Performance Analysis
    Togashi, Naohiro
    Klyuev, Vitaly
    2014 4TH IEEE INTERNATIONAL CONFERENCE ON INFORMATION SCIENCE AND TECHNOLOGY (ICIST), 2014, : 213 - 216
  • [25] The symbiosis of concurrency and verification: teaching and case studies
    Pedersen, Jan B.
    Welch, Peter H.
    FORMAL ASPECTS OF COMPUTING, 2018, 30 (02) : 239 - 277
  • [26] Automatic Verification of Erlang-Style Concurrency
    D'Osualdo, Emanuele
    Kochems, Jonathan
    Ong, C. -H. Luke
    STATIC ANALYSIS, SAS 2013, 2013, 7935 : 454 - 476
  • [27] Exploiting concurrency in system-on-chip verification
    Xu, Justin
    Lim, Cheng-Chew
    2006 IEEE ASIA PACIFIC CONFERENCE ON CIRCUITS AND SYSTEMS, 2006, : 836 - +
  • [28] Modular Verification of Concurrency-Aware Linearizability
    Hemed, Nir
    Rinetzky, Noam
    Vafeiadis, Viktor
    DISTRIBUTED COMPUTING (DISC 2015), 2015, 9363 : 371 - 387
  • [29] VERIFICATION - FORMAL OR OTHERWISE
    NEALE, RG
    ELECTRONIC ENGINEERING, 1994, 66 (811): : 5 - 5
  • [30] Formal Verification of Websites
    Flores, Sonia
    Lucas, Salvador
    Villanueva, Alicia
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2008, 200 (03) : 103 - 118
12345