Publication, Peng Li, Guodong Li and Ganesh Gopalakrishnan, Parametric Flows: Automated Behavior Equivalencing for Symbolic Analysis of Races in CUDA Programs. Supercomputing 2012, Salt Lake City, November 2012

Award, Professor Zvonimir Rakamarić received the Software Engineering Innovation Foundation (SEIF) award for his project: Analysis of Heterogeneous Concurrent Programs

Publication, A. Humphrey, Q. Meng, M. Berzins and T. Harman. Radiation Modeling Using the Uintah Heterogeneous CPU/GPU Runtime System. In Proceedings, XSEDE 2012

Publication, Guodong Li and Professor Ganesh Gopalakrishnan, Parameterized Verification of GPU Kernels, PLC Workshop 2012 (an IPDPS 2012 workshop)

Ganesh Gopalakrishnan, Formal Methods for Surviving the Jungle of Heterogeneous Parallelism, EduPar Poster (an IPDPS 2012 workshop)

Ganesh Gopalakrishnan and Tyler Sorensen, Integrating Formal Methods for Parallelism and Concurrency into Existing CS Curricula, EduPar Poster (an IPDPS 2012 workshop)

Invited Tutorial, Ganesh Gopalakrishnan, Safe March to Extreme-Scale Computing aided by Formal Methods, SJTU HPC Center, Shanghai Jiaotong University, May 2012

Conference paper, Peng Li, Guodong Li, and Ganesh Gopalakrishnan, Parametric Flows: Automated Behavior Equivalencing for Symbolic Analysis of Races in CUDA Programs, Supercomputing 2012, Salt Lake City, November 2012

Conference paper, Subodh Sharma, Ganesh Gopalakrishnan and Greg Bronevetsky, A Sound Reduction of Persistent-sets for Deadlock Detection in MPI Applications, SBMF 2012, Brazilian Symposium on Formal Methods, Natal, September 2012

Full Day Tutorial, Tobias Hilbrich, Ganesh Gopalakrishnan, Mathias S. Müller, Bronis R. de Supinski and David LeComber, Debugging MPI and CUDA at Scale, Supercomputing 2012, Salt Lake City, November 2012

Half Day Tutorial, Ganesh Gopalakrishnan, Symbolic Analysis of GPU Programs for Correctness and Performance, Formal Methods 2012, Paris, August 2012

Ganesh Gopalakrishnan delivered an invited talk, Formal Correctness Methods at the Million CPU Scale at INFINITY 2012 (FM 2012 Conference Workshop), Paris, August 2012

Publication, Guodong Li, Peng Li, Geof Sawaya, Indradeep Ghosh and Sreeranga P. Rajan, GKLEE: Concolic Verification and Test Genedration for GPUs, PPoPP, February, 2012. Paper PDF, Website for downloading full sources or a CDE package, and a Remote Execution Portal

Professor Mary Hall is leading the Performance Portability team of the SciDAC SUPER Project

Ganesh Gopalakrishnan lectured at UPMARC (in Bosön, Sweden) Multicore Computing Summer School on Formal Verification for High Performance Computing and XUM: An Experimental Multicore Supporting MCAPI

Ganesh Gopalakrishnan, Robert M. Kirby, Stephen Siegel, Rajeev Thakur, William Gropp, Ewing Lusk, Bronis R. de Supinski, Martin Schulz, and Greg Bronevetsky had their article Formal Analysis of MPI-Based Parallel Programs: Present and Future accepted to CACM: Communications of the ACM, June 2011

Anh Vo Successfully defended his PhD thesis titled Scalable Formal Dynamic Verification of MPI Programs through Distributed Causality Tracking, March, 2011

Stephen F. Siegel and Ganesh Gopalakrishnan, Formal Analysis of Message Passing, Invited Tutorial Paper, VMCAI 2011, Austin, Texas

Publication, Caitlin Sadowski, Thomas Ball, Judith Bishop, Sebastien Burckhardt, Ganesh Gopalakrishnan, Joseph Mayo, Madanlal Musuvathi, Shaz Qadeer and Stephe Toub, Practical parallel and concurrent programming. SIGSCE 2011: 189-194

Please visit our education page to read about Professor Gopalakrishnan's work on PPCP, or Practial Parallel and Concurrent Programming.

Guodong Li Successfully defended his PhD thesis titled Formal Verification of Programs and Their Transformations, August, 2010

Guodong Li presented his paper 'Scalable SMT-Based Verification of GPU Kernel Functions' at FSE-18

The Gauss Group presented a tutorial at SC 10: GEM: Graphical Explorer of MPI Programs

Anh Vo presented his paper 'A Scalable and Distributed Dynamic formal Verifier for MPI Programs' at SC 10

Alan Humphrey claimed second place in the overall student competition at SC 10 for his poster 'An Integration of Dynamic MPI Formal Verification Within Eclipse PTP'

Congratulations to Manu Awasthi, David Nellans, Kshitij Sudan, Rajeev Balasubramonian and Al Davis for their best paper award at PACT-19 (Parallel Architectures and Compilation Techniques) with their paper 'Handling the Problems and Opportunties Posed by Multiple On-Chip Memory Controllers'

Professor Mary Hall awarded $1.25M DARPA Grant

University of Utah selected for annual HP Labs Innovation Research Program -- Recipient: Prof. Rajeev Balasubramonian



Peter Neumann, SRI International Elliott Organick Memorial Lecture Series, March 26, 27, 2013. A Personal History of Layered Trustworthiness AND Clean-Slate Formally Motivated Hardware and Software for Highly Trustworthy Systems.

Manu Shantharam, PennState Center for Parallel computing at Utah Colloquium Series. Friday, May 11, 2012, 3:20 pm to 5:00 pm. 1230 WEB Application-aware strategies for managing performance and resilience tradeoffs

Norm Jouppi, HP Labs Colloquium. Wednesday, March 7, 2012. 1230 WEB. Future Computer Technologies and Their Architectural Implications

Torsten Hoefler, ETH Zurich Colloquium. Monday, January 23, 2012. 1230 WEB. Energy-aware Software Development for Massive-Scale Systems


Inanc Senocak, Boise State University Colloquium. Thursday, February 17, 2011, 3:20 pm to 5:00 pm 1250 WEB. title tba

Tom Ball, Microsoft Research CMSR/CPU Distinguished Lecture Series. Friday, November 12, 2010, 3:20 pm to 5:00 pm, 1250 WEB. Towards Scalable Modular Checking of Programs Against User-defined Properties

Tasneem Brutch, Samsung Research University of Utah, School of Computing Colloquium. Friday, November 5, 2010, 3:20 pm to 5:00 pm, 1250 WEB. Tool Interoperability Challenges and Approaches

Tim Mattson, Intel CMSR/CPU Distinguished Lecture Series. Friday, October 22, 2010, 3:20 pm to 5:00 pm, 1250 WEB. The future of many core processors: A Tale of Two Processors

Stephen Toub, Parallel Computing Platform team, Microsoft CMSR/CPU Distinguished Lecture Series. Friday, October 1, 2010, 3:20 pm to 5:00 pm, 1250 WEB. An Insider's View of Concurrency at Microsoft

Miriam Leeser, Northeastern University CMSR/CPU Distinguished Lecture Series. Wednesday, October 6, 2010, 3:20 pm to 5:00 pm, 103 WEB. GPU Programming and Correctness in Biomedical Applications

Shaz Qadeer, Microsoft Research CMSR/CPU Distinguished Lecture Series. Friday, September 24, 2010, 3:20 pm to 5:00 pm, 1250 WEB. QED: A Simplifier for Concurrent Programs

Ganesh Gopalakrishnan, University of Utah School of Computing Research Buffet. Wednesday, September 22, 2010, 3:50 pm to 5:00 pm; MEB 3167. Making Formal Methods Disappear

Madan Musuvathi, Microsoft Research CMSR/CPU Distinguished Lecture Series. Friday, September 17, 2010 3:20 pm to 5:00 pm 1250 WEB. Automatic Linearizability Checking for Concurrent Components

Sebastien Burkhardt, Microsoft Research CMSR/CPU Distinguished Lecture Series. Friday, September 10, 2010, 3:20 pm to 5:00 pm 1250 WEB. Concurrent Programming with Revisions

Miriam Leeser

Northeastern University

Wednesday, October 6, 2010
103 WEB
Refreshments 3:20 pm
Lecture 3:40 pm

GPU programming and correctness in Biomedical Applications


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.


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.