Publications

  • 2017

    • Rigorous Floating-point Mixed Precision Tuning
      Wei-Fan Chiang, Ganesh Gopalakrishnan, Zvonimir Rakamaric, Ian Briggs, Mark Stanisław Baranowski, Alexey Solovyev
      The 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL)
      January, 2017
  • 2016

    • PRESAGE: Protecting Structured Address Generation against Soft Errors
      Vishal Chandra Sharma, Ganesh Gopalakrishnan, Sriram Krishnamoorthy
      IEEE International Conference o High-Performance Computing, Data, and Analysis (HiPC)
      December, 2016
    • Portable Inter-Workgroup Barrier Synchronisation for GPUs [PDF]
      Tyler Sorenson, Alastair F. Donaldson, Mark Batty, Ganesh Gopalakrishnan, Zvonimir Rakamaric
      ACM SIGPLAN conference on Systems, Programming, Languages and Applications: Software for Humanity (SPLASH)
      November, 2016
    • ParFuse: Parallel and Compositional analysis of Message Passing Programs
      Sriram Aananthakrishnan, Greg Bronevetsky, Mark Stanisław Baranowski, Ganesh Gopalakrishnan
      The 29th International Workshop on Languages and Compilers for Parallel Computing
      September, 2016
      Related: [parfuse]
    • Toward Rigorous Design of Domain-Specific Distributed Systems [PDF]
      Mohammed Al-Mahfoudh, Ganesh Gopalakrishnan, Ryan Stutsman
      Workshop on Formal Methods in Software Engineering (FormaliSE)
      May, 2016
    • Towards Resiliency Evaluation of Vector Programs [PDF]
      Vishal Chandra Sharma, Ganesh Gopalakrishnan, Sriram Krishnamoorthy
      21st IEEE Workshop on Dependable Parallel, Distributed and Network-Centric Systems (DPDNS)
      May, 2016
    • ARCHER: Effectively Spotting Data Races in Large OpenMP Applications [PDF]
      Simone Atzeni, Ganesh Gopalakrishnan, Zvonimir Rakamaric, Dong H. Ahn, Gregory L Lee, Ignacio Laguna, Martin Schulz, Joachim Protze, Matthias Mueller
      30th IEEE International Parallel and Distributed Processing Symposium
      May, 2016
    • Formal Analysis Techniques for Reliable GPU programming: Current Solutions and Call to Action
      Alastair Donaldson, Ganesh Gopalakrishnan, Nathan Chong, Jeroen Ketema, Gudong Li, Peng Li, Anton Lokhmotov, Shaz Qadeer, Hamid Azad
      Advances in GPU Research and Practice
  • 2015

    • Unsafe Floating-point to Unsigned Integer Casting Check for GPU Programs [PDF]
      Wei-Fan Chiang, Ganesh Gopalakrishnan, Zvonimir Rakamaric
      8th International Workshop on Numerical Software Verification
      November, 2015
    • Practical Floating-Point Divergence Detection [PDF]
      Wei-Fan Chiang, Ganesh Gopalakrishnan, Zvonimir Rakamaric
      Languages and Compilers for Parallel Computing: 28th International Workshop, LCPC 2015
      September, 2015
    • Rigorous Estimation of Floating-Point Round-off Errors with Symbolic Taylor Expansions [PDF]
      Alexey Solovyev, Charles Jacobsen, Zvonimir Rakamaric, Ganesh Gopalakrishnan
      Proceedings of the 20th International Symposium on Formal Methods (FM)
      June, 2015
    • A Parameterized Floating-Point Formalization in {HOL} Light [PDF]
      Charles Jacobsen, Alexey Solovyev, Ganesh Gopalakrishnan
      NSV 2015: 8th International Workshop on Numerical Software Verification 2015
      April, 2015
    • GPU Concurrency: Weak Behaviours and Programming Assumptions [PDF]
      Jade Alglave, Mark Batty, Alastair F. Donaldson, Ganesh Gopalakrishnan, Jeroen Ketema, Daniel Poetzl, Tyler Sorensen, John Wickerson
      Proceedings of the Twentieth International Conference on Architectural Support for Programming Languages and Operating Systems
      March, 2015
  • 2014

    • Practical Symbolic Checking of GPU Programs [PDF]
      Peng Li, Guodong Li, Ganesh Gopalakrishnan
      Supercomputing
      November, 2014
    • Towards Providing Low-Overhead Data Race Detection for Large {OpenMP} Applications [PDF]
      Joachim Protze, Simone Atzeni, Dong H. Ahn, Martin Schulz and Ganesh Gopalakrishnan, Matthias S. Muller, Ignacio Laguna and Zvonimir Rakamaric, Greg L. Lee
      Proceedings of the LLVM Compiler Infrastructure in HPC Workshop (LLVM-HPC)
      November, 2014
    • Systematic Debugging of Concurrent Systems Using Coalesced Stack Trace Graphs [PDF]
      Diego Caminha B de Oliveira, Alan Humphrey, Qingyu Meng, Zvonimir Rakamaric, Martin Berzins, Ganesh Gopalakrishnan
      The 27th International Workshop on Languages and Compilers for Parallel Computing
      September, 2014
    • Systematic Debugging Methods for Large Scale HPC Computational Frameworks [PDF]
      Alan Humphrey, Qingyu Meng, Martin Berzins, Diego Caminha, Zvonimir Rakamarić, and Ganesh Gopalakrishnan
      Computing in Science Engineering
      June, 2014
    • FUSED: A Low-cost Online Soft-Error Detector [PDF]
      Vishal Chandra Sharma, Zvonimir Rakamaric, Ganesh Gopalakrishnan
      10th IEEE Workshop on Silicon Errors in Logic-System Effects (SELSE)
      March, 2014
    • Efficient Search for Inputs Causing High Floating-point Errors [PDF]
      Wei-Fan Chiang, Ganesh Gopalakrishnan, Zvonimir Rakamarić, and Alexey Solovyev
      Principles and Practices of Parallel Programming (PPoPP)
      January, 2014
  • 2013

    • Towards Formal Approaches to System Resilience
      Vishal Chandra Sharma, Arvind Haran, Zvonimir Rakamarić, Ganesh Gopalakrishnan
      19th IEEE Pacific Rim International Symposium on Dependable Computing (PRDC)
      December, 2013
    • Practical Formal Correctness Checking of Million-Core Problem Solving Environments for HPC [PDF]
      Diego Caminha, Ganesh Gopalakrishnan, Zvonimir Rakamarić, Martin Berzins, Alan Humphrey, Qingyu Meng
      7th International Workshop on Secure Software Engineering (SecSE)
      September, 2013
    • Hybrid Approach for Data-flow Analysis of MPI Programs
      Sriram Aananthakrishnan, Greg Bronevetsky, Ganesh Gopalakrishnan
      Proceedings of the 27th international ACM conference on International Conference on Supercomputing
      June, 2013
    • Formal Analysis of GPU Programs with Atomics via Conflict-Directed Delay-Bounding [PDF]
      Wei-Fan Chiang, Ganesh Gopalakrishnan, Zvonimir Rakamarić, Guodong Li
      NASA Formal Methods
      May, 2013
    • Determinism and Reproducibility in Large-Scale HPC Systems [PDF]
      Wei-Fan Chiang, Ganesh Gopalakrishnan, Zvonimir Rakamarić, Dong Ahn, Gregory Lee
      4th Workshop on Determinism and Correctness in Parallel Programming
      March, 2013
  • 2012

    • Parametric Flows: Automated Behavior Equivalencing for Symbolic Analysis of Races in CUDA Programs
      Peng Li, Guodong Li, Ganesh Gopalakrishnan
      Supercomputing
      November, 2012
    • A Sound Reduction of Persistent-sets for Deadlock Detection in MPI Applications
      Subodh Sharma, Ganesh Gopalakrishnan, Greg Bronevetsky
      SBMF 2012, Brazilian Symposium on Formal Methods
      September, 2012
    • MAAPED: Predictive Dynamic Analysis Tool for MPI Applications [PDF]
      Subodh Sharma, Ganesh Gopalakrishnan, Greg Bronevetsky
      SC Companion
      June, 2012
    • Parameterized Verification of GPU Kernels
      Guodong Li, Ganesh Gopalakrishnan
      PLC Workshop 2012 (an IPDPS 2012 workshop)
      May, 2012
    • Formal Methods for Surviving the Jungle of Heterogeneous Parallelism [PDF]
      Ganesh Gopalakrishnan
      IPDPS Workshops
      May, 2012
    • Formal Methods in System Design
      Ganesh Gopalakrishnan, Shaz Qadeer
      Formal Methods in System Design journal
      March, 2012
    • GKLEE: Concolic Verification and Test Generation for GPUs [PDF]
      Guodong Li, Peng Li, Geoffrey Sawaya, Ganesh Gopalakrishnan, Indradeep Ghosh, Sreeranga P. Rajan
      Principles and Practices of Parallel Programming (PPoPP)
      February, 2012
  • 2011

    • Formal Analysis of MPI-based Parallel Programs [PDF]
      Ganesh Gopalakrishnan, Robert Kirby, Stephen Siegel, Rajeev Thakur, William Gropp, Ewing Lusk, Bronis De Supinski, Martin Schulz, Greg Bronevetsky
      Communications of ACM
      December, 2011
    • Large Scale Verification of MPI Programs Using Lamport Clocks with Lazy Update [PDF]
      Anh Vo, Ganesh Gopalakrishnan, Robert M. Kirby, Bronis De Supinski, Martin Schulz, Greg Bronevetsky
      Parallel Architectures and Compilation Techniques
      October, 2011
    • Practical Parallel and Concurrent Programming [PDF]
      Caitlin Sadowski, Sebastian Burckhardt, Thomas Ball, Ganesh Gopalakrishnan, Judith Bishop, Joseph Mayo
      ACM SIGCSE
      May, 2011
    • Efficient Verification Solutions for Message Passing Systems [PDF]
      Subodh Sharma, Ganesh Gopalakrishnan
      IPDPS Workshops
      May, 2011
    • Formal Analysis of Message Passing [PDF]
      Stephen Siegel, Ganesh Gopalakrishnan
      Verification, Model Checking and Abstract Interpretation
      January, 2011
  • 2010

    • DAMPI: A Scalable and Distributed Dynamic Formal Verifier for MPI Programs [PDF]
      Anh Vo, Sriram Ananthakrishnan, Ganesh Gopalakrishnan, Bronis R. de Supinski
      Supercomputing
      November, 2010
    • Scalable SMT-Based Verification of GPU Kernel Functions [PDF]
      Guodong Li, Ganesh Gopalakrishnan
      FSE
      November, 2010
    • Top Ten Ways to Make Formal Methods for HPC Practical [PDF]
      Ganesh Gopalakrishnan, Robert M. Kirby
      SDP Workshop of FSE 2010
      November, 2010
    • GEM: Graphical Explorer of MPI Programs, [PDF]
      Alan Humphrey, Christopher Derrick, Ganesh Gopalakrishnan, Beth Tibbitts
      PSTI
      September, 2010
    • Precise Dynamic Analysis for Slack Elasticity: Adding Buffering Without Adding Bugs [PDF]
      Sarvani Vakkalanka, Anh Vo, Ganesh Gopalakrishnan, Robert M. Kirby
      EuroMPI
      September, 2010
    • Scalable Verification of MPI Programs [PDF]
      Anh Vo, Ganesh Gopalakrishnan
      IPDPS Workshops
      May, 2010
    • Distributed Dynamic Partial Order Reduction Based Verification of Threaded Software [PDF]
      Xiaofang Chen, Yu Yang, Ganesh Gopalakrishnan, Robert M. Kirby
      International Journal on Software Tools for Technology Transfer
      April, 2010
    • Efficient Methods for Formally Verifying Safety Properties of Hierarchical Cache Coherence Protocols [PDF]
      Xiaofang Chen, Yu Yang, Ganesh Gopalakrishnan, Ching-Tsun Chou
      Formal Methods in System Design
      March, 2010
    • PUG: A Symbolic Verifier of GPU Programs [PDF]
      Guodong Li, Ganesh Gopalakrishnan, Robert M. Kirby
      PPoPP workshop on GPGPUs
      January, 2010
    • A Symbolic Verifier for Cuda Programs
      Guodong Li, Ganesh Gopalakrishnan, Robert M. Kirby, Dan Quinlan
      Principles and Practices of Parallel Programming
      January, 2010
    • Formal methods applied to high-performance computing software design: a case study of MPI one-sided communication-based locking [PDF]
      Salman Pervez, Ganesh Gopalakrishnan, Robert M. Kirby, Rajeev Thakur, William Gropp
      Software Practice and Experience
      January, 2010
  • 2009

    • Reduced Execution Semantics of MPI: From theory to practice [PDF]
      Sarvani Vakkalanka, Anh Vo, Ganesh Gopalakrishnan, Robert M. Kirby
      Formal Methods (FM)
      November, 2009
    • MCC - A runtime verification tool for MCAPI user applications [PDF]
      Subodh Sharma, Ganesh Gopalakrishnan, Eric Mercer, Jim Holt
      Formal Methods in Computed Aidded Design
      November, 2009
    • Dynamic Verification of Multicore Communication Applictions in MCAPI, [PDF]
      Subodh Sharma, Ganesh Gopalakrishnan, Eric Mercer
      HLDVT
      November, 2009
    • Parallel and distributed model checking in Eddy [PDF]
      Igor Melatti, Robert Palmer, Geoffrey Sawaya, Yu Yang, Robert M. Kirby, Ganesh Gopalakrishnan
      Formal Methods in Computer Aided Design
      November, 2009
    • How Formal Dynamic Verification Tools Facilitate Novel Concurrency Visualizations [PDF]
      Sriram Aananthakrishnan, Michael DeLisi, Sarvani Vakkalanka, Anh Vo, Ganesh Gopalakrishnan, Robert M. Kirby, Rajeev Thakur
      EuroPVM/MPI
      September, 2009
    • Formal Verification of MCAPI Applications Using the Dynamic Verification tool MCC [PDF]
      Subodh Sharma, Ganesh Gopalakrishnan
      SRC Techcon
      September, 2009
    • Static-analysis Assisted Dynamic Verification to Efficiently Handle Waitany Non-determinism [PDF]
      Sarvani Vakkalanka, Grzegorz Szubzda, Anh Vo, Ganesh Gopalakrishnan, Robert M. Kirby, Rajeev Thakur
      EuroPVM/MPI
      September, 2009
    • Practical Formal Verification of MPI and Thread Programs [PDF]
      Ganesh Gopalakrishnan, Robert M. Kirby
      PVM/MPI (Book)
      September, 2009
    • Sound and Efficient Dynamic Verification of MPI Programs with Probe Non-Determinism [PDF]
      Anh Vo, Sarvani Vakkalanka, Jason Williams, Ganesh Gopalakrishnan, Robert M. Kirby, Rajeev Thakur
      EuroPVM/MPI
      September, 2009
    • Proceedings of the 7th Workshop on Parallel and Distributed Systems: Testing, Analysis, and Debugging, PADTAD 2009
      Ganesh Gopalakrishnan, Eitan Farchi, Eric Mercer
      PADTAD 2009
      July, 2009
    • Automatic Discovery of Transition Symmetry in Multithreaded Programs using Dynamic Analysis [PDF]
      Yu Yang, Xiaofang Chen, Ganesh Gopalakrishnan, Chao Wang
      SPIN
      June, 2009
    • Formal Verification of Practical MPI Programs [PDF]
      Anh Vo, Sarvani Vakkalanka, Michael DeLisi, Ganesh Gopalakrishnan, Robert M. Kirby, Rajeev Thakur
      Principles and Practices of Parallel Programming
      January, 2009
    • ISP Tool Update: Scalable MPI Verification [PDF]
      Anh Vo, Sarvani S. Vakkalanka, Ganesh Gopalakrishnan and
      Parallel Tools Workshop
      Dec, 2009
  • 2008

    • Dynamic Model Checking with Property Driven Pruning to Detect Race Conditions
      Chao Wang, Yu Yang, Aarti Gupta, Ganesh Gopalakrishnan
      ATVA
      October, 2008
    • A Formal Approach to Detect Functionally Irrelevant Barriers in MPI Programs [PDF]
      Subodh Sharma, Sarvani Vakkalanka, Ganesh Gopalakrishnan, Robert M. Kirby, Rajeev Thakur, William Gropp
      Recent Advances in Parallel Virtual Machine and Message Passing Interface (EuroPVM/MPI)
      September, 2008
    • Implementing Efficient Dynamic Formal Verification Methods for MPI Programs [PDF]
      Sarvani Vakkalanka, Michael DeLisi, Ganesh Gopalakrishnan, Robert M. Kirby, Rajeev Thakur, William Gropp
      Recent Advances in Parallel Virtual Machine and Message Passing Interface (EuroPVM/MPI)
      September, 2008
    • Review computation engineering: applied automata theory and logic [PDF]
      Ganesh Gopalakrishnan
      SIGACT
      September, 2008
    • Efficient Stateful Dynamic Partial Order Reduction [PDF]
      Yu Yang, Xiaofang Chen, Ganesh Gopalakrishnan, Robert M. Kirby
      Model Checking Software, 15th International SPIN Workshop
      August, 2008
    • Scheduling Considerations for Building Dynamic Verification Tools for MPI,” Parallel and Distributed Systems [PDF]
      Sarvani Vakkalanka, Michael DeLisi, Ganesh Gopalakrishnan, Robert M. Kirby
      Testing and Debugging (PADTAD-VI)
      July, 2008
    • Formal Specification of the MPI-2.0 Standard in TLA+ [PDF]
      Guodong Li, Michael DeLisi, Ganesh Gopalakrishnan, Robert M. Kirby
      Principles and Practices of Parallel Programming (PPoPP)
      February, 2008
    • ISP: A Tool for Model Checking MPI Programs [PDF]
      Sarvani Vakkalanka, Subodh Sharma, Ganesh Gopalakrishnan, Robert M. Kirby
      Principles and Practices of Parallel Programming (PPoPP)
      February, 2008
    • Dynamic Verification of MPI Programs with Reductions in Presence of Split Operations and Relaxed Orderings [PDF]
      Sarvani Vakkalanka, Ganesh Gopalakrishnan, Robert M. Kirby
      Computer Aided Verification
      January, 2008

For older publications, please visit our classic website