Abstract
GPUs are being used to accelerate many biomedical and scientific applications. My research group is accelerating applications including: i) lung tumor tracking to better pinpoint the tumor in radiation therapy and ii) in vivo imaging of tumors in live animals. In these and many other applications, high confidence in the correctness of the result is essential. At the same time, a GPU program is by its nature massively parallel, launching hundreds or thousands of threads simultaneously. Such programs are extremely difficult to debug. Symbolic methods are essential for reasoning about the concurrency inherent in these programs and their many different possible behaviors due to interleaving, memory interfacing and barrier synchronization. In this talk, I will discuss the applications we are working on, common coding errors in GPU programs, and why we believe that formal methods will help both finding bugs and giving users an increased confidence of the correctness of their GPU programs. We are also investigating arithmetic divergence between CPU and GPU code and how to characterize the errors between the two.

BIO
Professor Miriam Leeser received the BS degree in Electrical Engineering from Cornell University and the Diploma and PhD in Computer Science from Cambridge University in England. In 1992, she received a National Science Foundation CAREER award to conduct research into floating point arithmetic. She has been on the faculty of Northeastern since 1996, where she is head of the Reconfigurable Computing Laboratory and a member of the computer engineering research group and the Center for Communications and Digital Signal Processing. She is conducting research into accelerating image and signal processing applications with nontraditional computer architectures, including FPGAs, GPUs, and the Cell Broadband Engine. Her research includes building parameterized libraries and tools that enable application programmers to make use of highly optimized implementations developed for these platforms.