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 条

[31] Formal Verification of a Keystore
Boender, Jaap
Badevic, Goran
THEORETICAL ASPECTS OF SOFTWARE ENGINEERING, TASE 2022, 2022, 13299 : 49 - 64
[32] Formal verification at Intel
Harrison, J
18TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 2003, : 45 - 54
[33] Run-Time Verification of Optimistic Concurrency
Sezgin, Ali
Tasiran, Serdar
Muslu, Kivanc
Qadeer, Shaz
RUNTIME VERIFICATION, 2010, 6418 : 384 - +
[34] Safe Replication through Bounded Concurrency Verification
Kaki, Gowtham
Earanky, Kapil
Sivaramakrishnan, Kc
Jagannathan, Suresh
PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2018, 2 (OOPSLA):
[35] Formal verification of μ-charts
Goldson, D
APSEC 2002: NINTH ASIA PACIFIC SOFTWARE ENGINEERING CONFERENCE, 2002, : 129 - 136
[36] Formal verification of synchronizers
Kapschitz, T
Ginosar, R
CORRECT HARDWARE DESIGN AND VERIFICATION METHODS, PROCEEDINGS, 2005, 3725 : 359 - 362
[37] Formal Verification of HotStuff
Jehl, Leander
FORMAL TECHNIQUES FOR DISTRIBUTED OBJECTS, COMPONENTS, AND SYSTEMS, FORTE 2021, 2021, 12719 : 197 - 204
[38] Perspectives on Formal Verification
Friedman, Harvey M.
PROCEEDINGS OF THE 5TH ACM SIGPLAN CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS (CPP'16), 2016, : 1 - 1
[39] FORMAL VERIFICATION OF MICROPROCESSORS
SRIVAS, M
BICKFORD, M
COMPASS 89 : PROCEEDINGS OF THE FOURTH ANNUAL CONFERENCE ON COMPUTER ASSURANCE: SYSTEMS INTEGRITY, SOFTWARE SAFETY AND PROCESS SECURITY, 1989, : 93 - 102
[40] Formal Relationships Between Geometrical and Classical Models for Concurrency
Goubault, Eric
Mimram, Samuel
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2012, 283 : 77 - 109

← 1 2 3 4 5 →