Verification of Concurrent Go Programs using Timed Trace Theory

The Go programming language, or Go, plays a critical role in developing concurrent programs because it provides features such as goroutines and channels that support program concurrency. Even though concurrency makes programs efficient, verification is required to ensure their correctness. This paper proposes a novel approach to verifying concurrent Go programs using timed trace theory. The proposed approach is specifically designed to verify concurrent systems. Verifying a Go program using timed trace theory is divided into two tasks: modeling and verification. Modeling involves transforming a Go program into time Petri nets using a proposed algorithm. Verification involves checking the conformance between the Go program and its specification. This can be done automatically by the timed trace theoretic verification tool, which supports a partial order reduction technique to mitigate the state explosion problem. We demonstrate the verification of the Philosopher problem using both the total order method and the partial order reduction method. Experiments with the Go program of the Philosopher problem demonstrate the effectiveness of the proposed method.