Barnett, M., Evan Chang, B.-Y., DeLine, R., Jacobs, B. and Leino, K.R.M. (2005) Boogie: A Modular Reusable Verifier for Object-Oriented Programs. Vol. 4111, Springer, Berlin Heidelberg, 364-387.

has been cited by the following article:

• TITLE: Detecting Bank Conflict of GPU Programs Using Symbolic Execution—Case Study

  AUTHORS: Koki Hamaya, Satoshi Yamane

  KEYWORDS: Graphics Processing Units, GPU, Bank Conflict, Symbolic Execution, Model Checking

  JOURNAL NAME: Journal of Software Engineering and Applications, Vol.10 No.2, February 21, 2017

  ABSTRACT: GPU (Graphics Processing Unit) is used in various areas. Therefore, the demand for the verification of GPU programs is increasing. In this paper, we suggest the method to detect bank conflict by using symbolic execution. Bank conflict is one of the bugs happening in GPU and it leads the performance of programs lower. Bank conflict happens when some processing units in GPU access the same shared memory. Symbolic execution is the method to analysis programs with symbolic values. By using it, we can detect bank conflict on GPU programs which use many threads. We implement a prototype of the detector for bank conflict and evaluate it with some GPU programs. The result states that we can detect bank conflict on the programs with no loop regardless of the number of threads.