Formal verification of concurrency in go
Anuchit Prasertsang, Denduang Pradubsuwun · 2016
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.