Synthesizing Synchronous Digital VLSI Controllers Using Petri Nets. - Ganesh Gopalakrishnan (PNPM, 1987)

Design and Performance of Special Purpose Hardware for Time Warp. - Richard Fujimoto; Jya-Jang Tsai; Ganesh Gopalakrishnan (ISCA, 1988)

Implementing Functional Programs Using Mutable Abstract Data Types. - Ganesh Gopalakrishnan; Mandayam K. Srivas (Inf. Process. Lett., 1988)

Parallel Composition of Lockstep Synchronous Processes for Hardware Validation: Divide-and-Conquer Composition. - Ganesh Gopalakrishnan; Narayana Mani; Venkatesh Akella (Automatic Verification Methods for Finite State Systems, 1989)

HOP: A process model for synchronous hardware; semantics and experiments in process composition. - Ganesh Gopalakrishnan; Richard M. Fujimoto; Venkatesh Akella; Narayana Mani (Integr., 1989)

Towards a Verification Technique for Large Synchronous Circuits. - Prabhat Jain; Prabhakar Kudva; Ganesh Gopalakrishnan (CAV, 1992)

SHILPA: a high-level synthesis system for self-timed circuits. - Venkatesh Akella; Ganesh Gopalakrishnan (ICCAD, 1992)

Some Techniques for Efficient Symbolic Simulation-Based Verification. - Prabhat Jain; Ganesh Gopalakrishnan (ICCD, 1992)

Dynamic Reordering of Hgh Latency Transactions Using a Modified a Micropipeline. - Gernot Armin Liebchen; Ganesh Gopalakrishnan (ICCD, 1992)

From Process-Oriented Functional Specifications to Efficient Asynchronous Circuits. - Venkatesh Akella; Ganesh Gopalakrishnan (VLSI Design, 1992)

VLSI asynchronous systems: specification and synthesis. - Ganesh Gopalakrishnan; Venkatesh Akella (Microprocess. Microsystems, 1992)

Design and Evaluation of the Rollback Chip: Special Purpose Hardware for Time Warp. - Richard Fujimoto; Jya-Jang Tsai; Ganesh Gopalakrishnan (IEEE Trans. Computers, 1992)

Hierarchical Constraint Solving in the Parametric Form with Applications to Efficient Symbolic Simulation Based Verification. - Prabhat Jain; Ganesh Gopalakrishnan (ICCD, 1993)

A transformational approach to asynchronous high-level synthesis. - Ganesh Gopalakrishnan; Venkatesh Akella (VLSI, 1993)

Guest editors' introduction to the special issue on asynchronous systems. - Ganesh Gopalakrishnan; Erik Brunvand (Integr., 1993)

Design and Verification of the Rollback Chip Using HOP: A Case Study of Formal Methods Applied to Hardware design. - Ganesh Gopalakrishnan; Richard Fujimoto (ACM Trans. Comput. Syst., 1993)

Performance Analysis and Optimization of Asynchronous Circuits. - Prabhakar Kudva; Ganesh Gopalakrishnan; Erik Brunvand; Venkatesh Akella (ICCD, 1994)

Developing Micropipeline Wavefront Arbiters. - Ganesh Gopalakrishnan (IEEE Des. Test Comput., 1994)

CFSIM: A Concurrent Compiled Code Functional Simulator for hopCP. - Venkatesh Akella; Ganesh Gopalakrishnan (Int. J. Comput. Simul., 1994)

A correctness criterion for asynchronous circuit validation and optimization. - Ganesh Gopalakrishnan; Erik Brunvand; Nick Michell; Steven M. Nowick (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1994)

Efficient symbolic simulation-based verification using the parametric form of Boolean expressions. - Prabhat Jain; Ganesh Gopalakrishnan (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1994)

Specification and Validation of Control-Intensive IC's in hopCP. - Venkatesh Akella; Ganesh Gopalakrishnan (IEEE Trans. Software Eng., 1994)

High-level optimizations in compiling process descriptions to asynchronous circuits. - Ganesh Gopalakrishnan; Venkatesh Akella (J. VLSI Signal Process., 1994)

High speed counterflow-clocked pipelining illustrated on the design of HDTV subband vector quantizer chips. - Jae-Tack Yoo; Ganesh Gopalakrishnan; Kent F. Smith; V. John Mathews (ARVLSI, 1995)

A Technique for Synthesizing Distributed Burst-mode Circuits. - Prabhakar Kudva; Ganesh Gopalakrishnan; Hans M. Jacobson (DAC, 1996)

Synthesis for Hazard-free Customized CMOS Complex-Gate Networks Under Multiple-Input Changes. - Prabhakar Kudva; Ganesh Gopalakrishnan; Hans M. Jacobson; Steven M. Nowick (DAC, 1996)

Asynchronous Microengines for Efficient High-level Control. - Hans M. Jacobson; Ganesh Gopalakrishnan (ARVLSI, 1997)

Formal modeling and validation applied to a commercial coherent bus: a case study. - Ganesh Gopalakrishnan; Rajnish Ghughal; Ravi Hosabettu; Abdelillah Mokkedem; Ratan Nalumasu (CHARME, 1997)

A fast parallel squarer based on divide-and-conquer. - Jae-Tack Yoo; Kent F. Smith; Ganesh Gopalakrishnan (IEEE J. Solid State Circuits, 1997)

Decomposing the Proof of Correctness of pipelined Microprocessors. - Ravi Hosabettu; Mandayam K. Srivas; Ganesh Gopalakrishnan (CAV, 1998)

The 'Test Model-Checking' Approach to the Verification of Formal Memory Models of Multiprocessors. - Ratan Nalumasu; Rajnish Ghughal; Abdelillah Mokkedem; Ganesh Gopalakrishnan (CAV, 1998)

Formalization and Proof of a Solution to the PCI 2.1 Bus Transaction Ordering Problem. - Abdelillah Mokkedem; Ravi Hosabettu; Ganesh Gopalakrishnan (FMCAD, 1998)

PV: An Explicit Enumeration Model-Checker. - Ratan Nalumasu; Ganesh Gopalakrishnan (FMCAD, 1998)

Using "Test Model-Checking" to Verify the Runway-PA8000 Memory Model. - Rajnish Ghughal; Abdelillah Mokkedem; Ratan Nalumasu; Ganesh Gopalakrishnan (SPAA, 1998)

A Proof of Correctness of a Processor Implementing Tomasulo's Algorithm without a Reorder Buffer. - Ravi Hosabettu; Ganesh Gopalakrishnan; Mandayam K. Srivas (CHARME, 1999)

Application-specific programmable control for high-performance asynchronous circuits. - Hans M. Jacobson; Ganesh Gopalakrishnan (Proc. IEEE, 1999)

Corrections To application-specific Programmable Control For High-performance Asynchronous Circuits. - Hans M. Jacobson; Ganesh Gopalakrishnan (Proc. IEEE, 1999)

Peephole optimization of asynchronous macromodule networks. - Ganesh Gopalakrishnan; Prabhakar Kudva; Erik Brunvand (IEEE Trans. Very Large Scale Integr. Syst., 1999)

Timing constraints for high-speed counterflow-clocked pipelining. - Jae-Tack Yoo; Ganesh Gopalakrishnan; Kent F. Smith (IEEE Trans. Very Large Scale Integr. Syst., 1999)

High-Level Asynchronous System Design Using the ACK Framework. - Hans M. Jacobson; Erik Brunvand; Ganesh Gopalakrishnan; Prabhakar Kudva (ASYNC, 2000)

Verifying Advanced Microarchitectures that Support Speculation and Exceptions. - Ravi Hosabettu; Ganesh Gopalakrishnan; Mandayam K. Srivas (CAV, 2000)

Verifying Transaction Ordering Properties in Unbounded Bus Networks through Combined Deductive/Algorithmic Methods. - Michael D. Jones; Ganesh Gopalakrishnan (FMCAD, 2000)

Toward automated abstraction for protocols on branching networks. - Michael D. Jones; Ganesh Gopalakrishnan (HLDVT, 2000)

Achieving Fast and Exact Hazard-Free Logic Minimization of Extended Burst-Mode gC Finite State Machines. - Hans M. Jacobson; Chris J. Myers; Ganesh Gopalakrishnan (ICCAD, 2000)

Verification Methods for Weaker Shared Memory Consistency Models. - Rajnish Ghughal; Ganesh Gopalakrishnan (IPDPS Workshops, 2000)

Introduction: Formal Methods for CAD: Enabling Technologies and System-level Applications. - Ganesh Gopalakrishnan (Formal Methods Syst. Des., 2000)

Formalization and Analysis of a Solution to the PCI 2.1 Bus Transaction Ordering Problem. - Abdel Mokkedem; Ravi Hosabettu; Michael D. Jones; Ganesh Gopalakrishnan (Formal Methods Syst. Des., 2000)

Using live sequence charts for hardware protocol specification and compliance verification. - Annette Bunker; Ganesh Gopalakrishnan (HLDVT, 2001)

towards A formal Model of Shared Memory Consistency for Intel ItaniumTM. - Prosenjit Chatterjee; Ganesh Gopalakrishnan (ICCD, 2001)

Shared Memory Consistency Protocol Verification Against Weak Memory Models: Refinement via Model-Checking. - Prosenjit Chatterjee; Hemanthkumar Sivaraj; Ganesh Gopalakrishnan (CAV, 2002)

A Specification and Verification Framework for Developing Weak Shared Memory Consistency Protocols. - Prosenjit Chatterjee; Ganesh Gopalakrishnan (FMCAD, 2002)

A Distributed Partial Order Reduction Algorithm. - Robert Palmer; Ganesh Gopalakrishnan (FORTE, 2002)

FSRC: fair and stable rate control - a TCP-friendly adaptive rate control scheme for packet audio applications. - Syam Krishna Babbellapati; Ganesh Gopalakrishnan; T. S. Lamba (ICON, 2002)

Specifying Java thread semantics using a uniform memory model. - Yue Yang; Ganesh Gopalakrishnan; Gary Lindstrom (Java Grande, 2002)

Incremental Proof of the Producer/Consumer Property for the PCI Protocol. - Dominique Cansell; Ganesh Gopalakrishnan; Michael D. Jones; Dominique Méry; Airy Weinzoepflen (ZB, 2002)

Robust rate based congestion control. - Ganesh Gopalakrishnan; Sneha Kumar Kasera (Comput. Commun. Rev., 2002)

Deriving Efficient Cache Coherence Protocols Through Refinement. - Ratan Nalumasu; Ganesh Gopalakrishnan (Formal Methods Syst. Des., 2002)

An Efficient Partial Order Reduction Algorithm with an Alternative Proviso Implementation. - Ratan Nalumasu; Ganesh Gopalakrishnan (Formal Methods Syst. Des., 2002)

Analyzing the Intel Itanium Memory Ordering Rules Using Logic Programming and SAT. - Yue Yang; Ganesh Gopalakrishnan; Gary Lindstrom; Konrad Slind (CHARME, 2003)

A Practical Methodology for Verifying Pipelined Microarchitectures. - Ravi Hosabettu; Ganesh Gopalakrishnan; Mandayam K. Srivas (IEEE Des. Test Comput., 2003)

Random Walk Based Heuristic Algorithms for Distributed Memory Model Checking. - Hemanthkumar Sivaraj; Ganesh Gopalakrishnan (PDMC@CAV, 2003)

Industrial Practice of Formal Hardware Verification: A Sampling. - Ganesh Gopalakrishnan; Warren A. Hunt Jr. (Formal Methods Syst. Des., 2003)

Formal Verification of a Complex Pipelined Processor. - Ravi Hosabettu; Ganesh Gopalakrishnan; Mandayam K. Srivas (Formal Methods Syst. Des., 2003)

QB or Not QB: An Efficient Execution Verification Tool for Memory Orderings. - Ganesh Gopalakrishnan; Yue Yang; Hemanthkumar Sivaraj (CAV, 2004)

Memory-Model-Sensitive Data Race Analysis. - Yue Yang; Ganesh Gopalakrishnan; Gary Lindstrom (ICFEM, 2004)

Nemos: A Framework for Axiomatic and Executable Specifications of Memory Consistency Models. - Yue Yang; Ganesh Gopalakrishnan; Gary Lindstrom; Konrad Slind (IPDPS, 2004)

Formal hardware specification languages for protocol compliance verification. - Annette Bunker; Ganesh Gopalakrishnan; Sally A. McKee (ACM Trans. Design Autom. Electr. Syst., 2004)

Symbolic Partial Order Reduction for Rule Based Transition Systems. - Ritwik Bhattacharya; Steven M. German; Ganesh Gopalakrishnan (CHARME, 2005)

Counterexample Guided Invariant Discovery for Parameterized Cache Coherence Verification. - Sudhindra Pandav; Konrad Slind; Ganesh Gopalakrishnan (CHARME, 2005)

On the decidability of shared memory consistency verification. - Ali Sezgin; Ganesh Gopalakrishnan (MEMOCODE, 2005)

UMM: an operational memory model specification framework with integrated model checking capability. - Yue Yang; Ganesh Gopalakrishnan; Gary Lindstrom (Concurr. Pract. Exp., 2005)

Gauss: A Framework for Verifying Scientific Computing Software. - Robert Palmer; Steve Barrus; Yu Yang 013; Ganesh Gopalakrishnan; Robert M. Kirby (SoftMC@CAV, 2005)

On the definition of sequential consistency. - Ali Sezgin; Ganesh Gopalakrishnan (Inf. Process. Lett., 2005)

Live sequence charts applied to hardware requirements specification and verification. - Annette Bunker; Ganesh Gopalakrishnan; Konrad Slind (Int. J. Softw. Tools Technol. Transf., 2005)

Computation engineering - applied automata theory and logic. - Ganesh Gopalakrishnan (Springer, 2006)

Reducing Verification Complexity of a Multicore Coherence Protocol Using Assume/Guarantee. - Xiaofang Chen; Yu Yang 013; Ganesh Gopalakrishnan; Ching-Tsun Chou (FMCAD, 2006)

Toward reliable and efficient message passing software through formal analysis. - Ganesh Gopalakrishnan; Robert M. Kirby (IPDPS, 2006)

Formal Verification of Programs That Use MPI One-Sided Communication. - Salman Pervez; Ganesh Gopalakrishnan; Robert M. Kirby; Rajeev Thakur; William D. Gropp (PVM/MPI, 2006)

Exploiting Symmetry and Transactions for Partial Order Reduction of Rule Based Specifications. - Ritwik Bhattacharya; Steven M. German; Ganesh Gopalakrishnan (SPIN, 2006)

Preface. - Ganesh Gopalakrishnan; John O'Leary (TV@FLoC, 2006)

Transaction Based Modeling and Verification of Hardware Protocols. - Xiaofang Chen; Steven M. German; Ganesh Gopalakrishnan (FMCAD, 2007)

An Approach to Formalization and Analysis of Message Passing Libraries. - Robert Palmer; Michael Delisi; Ganesh Gopalakrishnan; Robert M. Kirby (FMICS, 2007)

Hierarchical cache coherence protocol verification one level at a time through assume guarantee. - Xiaofang Chen; Yu Yang 013; Michael Delisi; Ganesh Gopalakrishnan; Ching-Tsun Chou (HLDVT, 2007)

Formal Analysis for Debugging and Performance Optimization of MPI. - Ganesh Gopalakrishnan; Robert M. Kirby (IPDPS, 2007)

Semantics driven dynamic partial-order reduction of MPI-based parallel programs. - Robert Palmer; Ganesh Gopalakrishnan; Robert M. Kirby (PADTAD, 2007)

Practical Model-Checking Method for Verifying Correctness of MPI Programs. - Salman Pervez; Ganesh Gopalakrishnan; Robert M. Kirby; Robert Palmer; Rajeev Thakur; William Gropp (PVM/MPI, 2007)

Distributed Dynamic Partial Order Reduction Based Verification of Threaded Software. - Yu Yang 013; Xiaofang Chen; Ganesh Gopalakrishnan; Robert M. Kirby (SPIN, 2007)

Preface. - Ganesh Gopalakrishnan (Festschrift honoring Gary Lindstrom, 2007)

Formal Methods for MPI Programs. - Ganesh Gopalakrishnan; Robert M. Kirby (Festschrift honoring Gary Lindstrom, 2007)

Dynamic Model Checking with Property Driven Pruning to Detect Race Conditions. - Chao Wang 001; Yu Yang 013; Aarti Gupta; Ganesh Gopalakrishnan (ATVA, 2008)

Dynamic Verification of MPI Programs with Reductions in Presence of Split Operations and Relaxed Orderings. - Sarvani S. Vakkalanka; Ganesh Gopalakrishnan; Robert M. Kirby (CAV, 2008)

Runtime verification methods for MPI. - Ganesh Gopalakrishnan; Robert M. Kirby (IPDPS, 2008)

Scheduling considerations for building dynamic verification tools for MPI. - Sarvani S. Vakkalanka; Michael Delisi; Ganesh Gopalakrishnan; Robert M. Kirby (PADTAD, 2008)

Formal specification of the MPI-2.0 standard in TLA+. - Guodong Li; Michael Delisi; Ganesh Gopalakrishnan; Robert M. Kirby (PPoPP, 2008)

ISP: a tool for model checking MPI programs. - Sarvani S. Vakkalanka; Subodh Sharma 001; Ganesh Gopalakrishnan; Robert M. Kirby (PPoPP, 2008)

A Formal Approach to Detect Functionally Irrelevant Barriers in MPI Programs. - Subodh Sharma 001; Sarvani S. Vakkalanka; Ganesh Gopalakrishnan; Robert M. Kirby; Rajeev Thakur; William Gropp (PVM/MPI, 2008)

Implementing Efficient Dynamic Formal Verification Methods for MPI Programs. - Sarvani S. Vakkalanka; Michael Delisi; Ganesh Gopalakrishnan; Robert M. Kirby; Rajeev Thakur; William Gropp (PVM/MPI, 2008)

Efficient Stateful Dynamic Partial Order Reduction. - Yu Yang 013; Xiaofang Chen; Ganesh Gopalakrishnan; Robert M. Kirby (SPIN, 2008)

Review computation engineering: applied automata theory and logic. - Ganesh Gopalakrishnan (SIGACT News, 2008)

Reduced Execution Semantics of MPI: From Theory to Practice. - Sarvani S. Vakkalanka; Anh Vo; Ganesh Gopalakrishnan; Robert M. Kirby (FM, 2009)

MCC: A runtime verification tool for MCAPI user applications. - Subodh Sharma 001; Ganesh Gopalakrishnan; Eric Mercer; Jim Holt (FMCAD, 2009)

Dynamic verification of Multicore Communication applications in MCAPI. - Subodh Sharma 001; Ganesh Gopalakrishnan; Eric Mercer (HLDVT, 2009)

Some resources for teaching concurrency. - Ganesh Gopalakrishnan; Yu Yang 013; Sarvani S. Vakkalanka; Anh Vo; Sriram Aananthakrishnan; Grzegorz Szubzda; Geoffrey Sawaya; Jason Williams; Subodh Sharma 001; Michael Delisi; Simone Atzeni (PADTAD, 2009)

Formal verification of practical MPI programs. - Anh Vo; Sarvani S. Vakkalanka; Michael Delisi; Ganesh Gopalakrishnan; Robert M. Kirby; Rajeev Thakur (PPoPP, 2009)

ISP Tool Update: Scalable MPI Verification. - Anh Vo; Sarvani S. Vakkalanka; Ganesh Gopalakrishnan (Parallel Tools Workshop, 2009)

How Formal Dynamic Verification Tools Facilitate Novel Concurrency Visualizations. - Sriram Aananthakrishnan; Michael Delisi; Sarvani S. Vakkalanka; Anh Vo; Ganesh Gopalakrishnan; Robert M. Kirby; Rajeev Thakur (PVM/MPI, 2009)

Practical Formal Verification of MPI and Thread Programs. - Ganesh Gopalakrishnan; Robert M. Kirby (PVM/MPI, 2009)

Static-Analysis Assisted Dynamic Verification of MPI Waitany Programs (Poster Abstract). - Sarvani S. Vakkalanka; Grzegorz Szubzda; Anh Vo; Ganesh Gopalakrishnan; Robert M. Kirby; Rajeev Thakur (PVM/MPI, 2009)

Sound and Efficient Dynamic Verification of MPI Programs with Probe Non-determinism. - Anh Vo; Sarvani S. Vakkalanka; Jason Williams; Ganesh Gopalakrishnan; Robert M. Kirby; Rajeev Thakur (PVM/MPI, 2009)

Automatic Discovery of Transition Symmetry in Multithreaded Programs Using Dynamic Analysis. - Yu Yang 013; Xiaofang Chen; Ganesh Gopalakrishnan; Chao Wang 001 (SPIN, 2009)

Parallel and distributed model checking in Eddy. - Igor Melatti; Robert Palmer; Geoffrey Sawaya; Yu Yang 013; Robert M. Kirby; Ganesh Gopalakrishnan (Int. J. Softw. Tools Technol. Transf., 2009)

GEM: Graphical Explorer of MPI Programs. - Alan Humphrey; Christopher Derrick; Ganesh Gopalakrishnan; Beth Tibbitts (ICPP Workshops, 2010)

Scalable verification of MPI programs. - Anh Vo; Ganesh Gopalakrishnan (IPDPS Workshops, 2010)

A symbolic verifier for CUDA programs. - Guodong Li; Ganesh Gopalakrishnan; Robert M. Kirby; Daniel J. Quinlan (PPoPP, 2010)

Dynamic Verification of Hybrid Programs. - Wei-Fan Chiang; Grzegorz Szubzda; Ganesh Gopalakrishnan; Rajeev Thakur (EuroMPI, 2010)

Precise Dynamic Analysis for Slack Elasticity: Adding Buffering without Adding Bugs. - Sarvani S. Vakkalanka; Anh Vo; Ganesh Gopalakrishnan; Robert M. Kirby (EuroMPI, 2010)

A Scalable and Distributed Dynamic Formal Verifier for MPI Programs. - Anh Vo; Sriram Aananthakrishnan; Ganesh Gopalakrishnan; Bronis R. de Supinski; Martin Schulz 001; Greg Bronevetsky (SC, 2010)

Top ten ways to make formal methods for HPC practical. - Ganesh Gopalakrishnan; Robert M. Kirby (FoSER, 2010)

Scalable SMT-based verification of GPU kernel functions. - Guodong Li; Ganesh Gopalakrishnan (SIGSOFT FSE, 2010)

Efficient methods for formally verifying safety properties of hierarchical cache coherence protocols. - Xiaofang Chen; Yu Yang 013; Ganesh Gopalakrishnan; Ching-Tsun Chou (Formal Methods Syst. Des., 2010)

Formal methods applied to high-performance computing software design: a case study of MPI one-sided communication-based locking. - Salman Pervez; Ganesh Gopalakrishnan; Robert M. Kirby; Rajeev Thakur; William Gropp (Softw. Pract. Exp., 2010)

Distributed dynamic partial order reduction. - Yu Yang 013; Xiaofang Chen; Ganesh Gopalakrishnan; Robert M. Kirby (Int. J. Softw. Tools Technol. Transf., 2010)

Large Scale Verification of MPI Programs Using Lamport Clocks with Lazy Update. - Anh Vo; Ganesh Gopalakrishnan; Robert M. Kirby; Bronis R. de Supinski; Martin Schulz 001; Greg Bronevetsky (PACT, 2011)

Efficient Verification Solutions for Message Passing Systems. - Subodh Sharma 001; Ganesh Gopalakrishnan (IPDPS Workshops, 2011)

Practical parallel and concurrent programming. - Caitlin Sadowski; Thomas Ball 001; Judith Bishop; Sebastian Burckhardt; Ganesh Gopalakrishnan; Joseph Mayo; Madanlal Musuvathi; Shaz Qadeer; Stephen Toub (SIGCSE, 2011)

Formal Analysis of Message Passing - (Invited Talk). - Stephen F. Siegel; Ganesh Gopalakrishnan (VMCAI, 2011)

Formal analysis of MPI-based parallel programs. - Ganesh Gopalakrishnan; Robert M. Kirby; Stephen F. Siegel; Rajeev Thakur; William Gropp; Ewing L. Lusk; Bronis R. de Supinski; Martin Schulz 001; Greg Bronevetsky (Commun. ACM, 2011)

Formal specification of MPI 2.0: Case study in specifying a practical concurrent programming API. - Guodong Li; Robert Palmer; Michael Delisi; Ganesh Gopalakrishnan; Robert M. Kirby (Sci. Comput. Program., 2011)

Formal Methods for Surviving the Jungle of Heterogeneous Parallelism. - Ganesh Gopalakrishnan (IPDPS Workshops, 2012)

Parameterized Verification of GPU Kernel Programs. - Guodong Li; Ganesh Gopalakrishnan (IPDPS Workshops, 2012)

GKLEE: concolic verification and test generation for GPUs. - Guodong Li; Peng Li 058; Geoffrey Sawaya; Ganesh Gopalakrishnan; Indradeep Ghosh; Sreeranga P. Rajan (PPoPP, 2012)

A Sound Reduction of Persistent-Sets for Deadlock Detection in MPI Applications. - Subodh Sharma 001; Ganesh Gopalakrishnan; Greg Bronevetsky (SBMF, 2012)

Parametric flows: automated behavior equivalencing for symbolic analysis of races in CUDA programs. - Peng Li 058; Guodong Li; Ganesh Gopalakrishnan (SC, 2012)

Abstract: MAPPED: Predictive Dynamic Analysis Tool for MPI Applications. - Subodh Sharma 001; Ganesh Gopalakrishnan; Greg Bronevetsky (SC Companion, 2012)

Preface. - Ganesh Gopalakrishnan; Shaz Qadeer (Formal Methods Syst. Des., 2012)

Visual analysis of uncertainties in ocean forecasts for planning and operation of off-shore structures. - Thomas Höllt; Ahmed Magdy; Guoning Chen; Ganesh Gopalakrishnan; Ibrahim Hoteit; Charles D. Hansen; Markus Hadwiger (PacificVis, 2013)

Hybrid approach for data-flow analysis of MPI programs. - Sriram Aananthakrishnan; Greg Bronevetsky; Ganesh Gopalakrishnan (ICS, 2013)

Towards shared memory consistency models for GPUs. - Tyler Sorensen 001; Ganesh Gopalakrishnan; Vinod Grover (ICS, 2013)

Practical formal correctness checking of million-core problem solving environments for HPC. - Diego Caminha Barbosa De Oliveira; Zvonimir Rakamaric; Ganesh Gopalakrishnan; Alan Humphrey; Qingyu Meng; Martin Berzins (SE-CSE@ICSE, 2013)

Formal Analysis of GPU Programs with Atomics via Conflict-Directed Delay-Bounding. - Wei-Fan Chiang; Ganesh Gopalakrishnan; Guodong Li; Zvonimir Rakamaric (NASA Formal Methods, 2013)

Towards Formal Approaches to System Resilience. - Vishal Chandra Sharma; Arvind Haran; Zvonimir Rakamaric; Ganesh Gopalakrishnan (PRDC, 2013)

Overcoming extreme-scale reproducibility challenges through a unified, targeted, and multilevel toolset. - Dong H. Ahn; Gregory L. Lee; Ganesh Gopalakrishnan; Zvonimir Rakamaric; Martin Schulz 001; Ignacio Laguna (SE-HPCCSE@SC, 2013)

Systematic Debugging of Concurrent Systems Using Coalesced Stack Trace Graphs. - Diego Caminha Barbosa De Oliveira; Zvonimir Rakamaric; Ganesh Gopalakrishnan; Alan Humphrey; Qingyu Meng; Martin Berzins (LCPC, 2014)

Efficient search for inputs causing high floating-point errors. - Wei-Fan Chiang; Ganesh Gopalakrishnan; Zvonimir Rakamaric; Alexey Solovyev (PPoPP, 2014)

Practical Symbolic Race Checking of GPU Programs. - Peng Li 058; Guodong Li; Ganesh Gopalakrishnan (SC, 2014)

Towards providing low-overhead data race detection for large OpenMP applications. - Joachim Protze; Simone Atzeni; Dong H. Ahn; Martin Schulz 001; Ganesh Gopalakrishnan; Matthias S. Müller; Ignacio Laguna; Zvonimir Rakamaric; Gregory L. Lee (LLVM@SC, 2014)

Systematic Debugging Methods for Large-Scale HPC Computational Frameworks. - Alan Humphrey; Qingyu Meng; Martin Berzins; Diego Caminha Barbosa De Oliveira; Zvonimir Rakamaric; Ganesh Gopalakrishnan (Comput. Sci. Eng., 2014)

Unsafe Floating-point to Unsigned Integer Casting Check for GPU Programs. - Wei-Fan Chiang; Ganesh Gopalakrishnan; Zvonimir Rakamaric (NSV, 2014)

Ovis: A Framework for Visual Analysisof Ocean Forecast Ensembles. - Thomas Höllt; Ahmed Magdy; Peng Zhan; Guoning Chen; Ganesh Gopalakrishnan; Ibrahim Hoteit; Charles D. Hansen; Markus Hadwiger (IEEE Trans. Vis. Comput. Graph., 2014)

GPU Concurrency: Weak Behaviours and Programming Assumptions. - Jade Alglave; Mark Batty; Alastair F. Donaldson; Ganesh Gopalakrishnan; Jeroen Ketema; Daniel Poetzl; Tyler Sorensen 001; John Wickerson (ASPLOS, 2015)

Rigorous Estimation of Floating-Point Round-off Errors with Symbolic Taylor Expansions. - Alexey Solovyev; Charles Jacobsen; Zvonimir Rakamaric; Ganesh Gopalakrishnan (FM, 2015)

Achieving Formal Parallel Program Debugging by Incentivizing CS/HPC Collaborative Tool Development. - Ganesh Gopalakrishnan; Geof Sawaya (SCREAM@HPDC, 2015)

Practical Floating-Point Divergence Detection. - Wei-Fan Chiang; Ganesh Gopalakrishnan; Zvonimir Rakamaric (LCPC, 2015)

A Parameterized Floating-Point Formalizaton in HOL Light. - Charles Jacobsen; Alexey Solovyev; Ganesh Gopalakrishnan (NSV, 2015)

PRESAGE: Protecting Structured Address Generation against Soft Errors. - Vishal Chandra Sharma; Ganesh Gopalakrishnan; Sriram Krishnamoorthy (HiPC, 2016)

Toward rigorous design of domain-specific distributed systems. - Mohammed Al-Mahfoudh; Ganesh Gopalakrishnan; Ryan Stutsman (FormaliSE@ICSE, 2016)

ARCHER: Effectively Spotting Data Races in Large OpenMP Applications. - Simone Atzeni; Ganesh Gopalakrishnan; Zvonimir Rakamaric; Dong H. Ahn; Ignacio Laguna; Martin Schulz 001; Gregory L. Lee; Joachim Protze; Matthias S. Müller (IPDPS, 2016)

Towards Resiliency Evaluation of Vector Programs. - Vishal Chandra Sharma; Ganesh Gopalakrishnan; Sriram Krishnamoorthy (IPDPS Workshops, 2016)

Toward Bringing Distributed System Design upon Rigorous Footing. - Mohammed S. Al-Mahfoudh; Ganesh Gopalakrishnan; Ryan Stutsman (IRI, 2016)

ParFuse: Parallel and Compositional Analysis of Message Passing Programs. - Sriram Aananthakrishnan; Greg Bronevetsky; Mark Baranowski; Ganesh Gopalakrishnan (LCPC, 2016)

Portable inter-workgroup barrier synchronisation for GPUs. - Tyler Sorensen 001; Alastair F. Donaldson; Mark Batty; Ganesh Gopalakrishnan; Zvonimir Rakamaric (OOPSLA, 2016)

FLiT: Cross-platform floating-point result-consistency tester and workload. - Geoffrey Sawaya; Michael Bentley; Ian Briggs; Ganesh Gopalakrishnan; Dong H. Ahn (IISWC, 2017)

Moving the Needle on Rigorous Floating-Point Precision Tuning. - Marek S. Baranowski; Ian Briggs; Wei-Fan Chiang; Ganesh Gopalakrishnan; Zvonimir Rakamaric; Alexey Solovyev (AFM@NFM, 2017)

Rigorous floating-point mixed-precision tuning. - Wei-Fan Chiang; Mark Baranowski; Ian Briggs; Alexey Solovyev; Ganesh Gopalakrishnan; Zvonimir Rakamaric (POPL, 2017)

Report of the HPC Correctness Summit, Jan 25-26, 2017, Washington, DC. - Ganesh Gopalakrishnan; Paul D. Hovland; Costin Iancu; Sriram Krishnamoorthy; Ignacio Laguna; Richard A. Lethin; Koushik Sen; Stephen F. Siegel; Armando Solar-Lezama (CoRR, 2017)

An Operational Semantic Basis for OpenMP Race Analysis. - Simone Atzeni; Ganesh Gopalakrishnan (CoRR, 2017)

An Operational Semantic Basis for Building an OpenMP Data Race Checker. - Simone Atzeni; Ganesh Gopalakrishnan (IPDPS Workshops, 2018)

SWORD: A Bounded Memory-Overhead Detector of OpenMP Data Races in Production Runs. - Simone Atzeni; Ganesh Gopalakrishnan; Zvonimir Rakamaric; Ignacio Laguna; Gregory L. Lee; Dong H. Ahn (IPDPS, 2018)

Using Deep Learning for Automated Communication Pattern Characterization: Little Steps and Big Challenges. - Philip C. Roth; Kevin A. Huck; Ganesh Gopalakrishnan; Felix Wolf 001 (ESPT/VPA@SC, 2018)

ParLoT: Efficient Whole-Program Call Tracing for HPC Applications. - Saeed Taheri; Sindhu Devale; Ganesh Gopalakrishnan; Martin Burtscher (ESPT/VPA@SC, 2018)

Sparse Matrix Code Dependence Analysis Simplification at Compile Time. - Mahdi Soltan Mohammadi; Kazem Cheshmi; Ganesh Gopalakrishnan; Mary W. Hall; Maryam Mehri Dehnavi; Anand Venkat; Tomofumi Yuki; Michelle Mills Strout (CoRR, 2018)

DiffTrace: Efficient Whole-Program Trace Analysis and Diffing for Debugging. - Saeed Taheri; Ian Briggs; Martin Burtscher; Ganesh Gopalakrishnan (CLUSTER, 2019)

Multi-Level Analysis of Compiler-Induced Variability and Performance Tradeoffs. - Michael Bentley; Ian Briggs; Ganesh Gopalakrishnan; Dong H. Ahn; Ignacio Laguna; Gregory L. Lee; Holger E. Jones (HPDC, 2019)

Message Scheduling for Performant, Many-Core Belief Propagation. - Mark Van der Merwe; Vinu Joseph; Ganesh Gopalakrishnan (HPEC, 2019)

A Programmable Approach to Model Compression. - Vinu Joseph; Saurav Muralidharan; Animesh Garg; Michael Garland; Ganesh Gopalakrishnan (CoRR, 2019)

Pruners. - Kento Sato; Ignacio Laguna; Gregory L. Lee; Martin Schulz 001; Christopher M. Chambreau; Simone Atzeni; Michael Bentley; Ganesh Gopalakrishnan; Zvonimir Rakamaric; Geof Sawaya; Joachim Protze; Dong H. Ahn (Int. J. High Perform. Comput. Appl., 2019)

Rigorous Estimation of Floating-Point Round-Off Errors with Symbolic Taylor Expansions. - Alexey Solovyev; Marek S. Baranowski; Ian Briggs; Charles Jacobsen; Zvonimir Rakamaric; Ganesh Gopalakrishnan (ACM Trans. Program. Lang. Syst., 2019)

ArcherGear: data race equivalencing for expeditious HPC debugging. - Samuel Thayer; Ganesh Gopalakrishnan; Ian Briggs; Michael Bentley; Dong H. Ahn; Ignacio Laguna; Gregory L. Lee (PPoPP, 2020)

Scalable yet rigorous floating-point error analysis. - Arnab Das; Ian Briggs; Ganesh Gopalakrishnan; Sriram Krishnamoorthy; Pavel Panchekha (SC, 2020)

Correctness-preserving Compression of Datasets and Neural Network Models. - Vinu Joseph; Nithin Chalapathi; Aditya Bhaskara; Ganesh Gopalakrishnan; Pavel Panchekha; Mu Zhang 001 (CORRECTNESS@SC, 2020)

An Abstraction-guided Approach to Scalable and Rigorous Floating-Point Error Analysis. - Arnab Das; Ian Briggs; Ganesh Gopalakrishnan; Sriram Krishnamoorthy (CoRR, 2020)

Reliable Model Compression via Label-Preservation-Aware Loss Functions. - Vinu Joseph; Shoaib Ahmed Siddiqui; Aditya Bhaskara; Ganesh Gopalakrishnan; Saurav Muralidharan; Michael Garland; Sheraz Ahmed; Andreas Dengel 001 (CoRR, 2020)

A Programmable Approach to Neural Network Compression. - Vinu Joseph; Ganesh Gopalakrishnan; Saurav Muralidharan; Michael Garland; Animesh Garg (IEEE Micro, 2020)

FailAmp: Relativization Transformation for Soft Error Detection in Structured Address Generation. - Ian Briggs; Arnab Das; Mark Baranowski; Vishal Chandra Sharma; Sriram Krishnamoorthy; Zvonimir Rakamaric; Ganesh Gopalakrishnan (ACM Trans. Archit. Code Optim., 2020)

FPDetect: Efficient Reasoning About Stencil Programs Using Selective Direct Evaluation. - Arnab Das; Sriram Krishnamoorthy; Ian Briggs; Ganesh Gopalakrishnan; Ramakrishna Tipireddy (ACM Trans. Archit. Code Optim., 2020)

Robustness Analysis of Loop-Free Floating-Point Programs via Symbolic Automatic Differentiation. - Arnab Das; Tanmay Tirpankar; Ganesh Gopalakrishnan; Sriram Krishnamoorthy (CLUSTER, 2021)

Guarding Numerics Amidst Rising Heterogeneity. - Ganesh Gopalakrishnan; Ignacio Laguna; Ang Li 006; Pavel Panchekha; Cindy Rubio-González; Zachary Tatlock (Correctness@SC, 2021)

GoAT: Automated Concurrency Analysis and Debugging Tool for Go. - Saeed Taheri; Ganesh Gopalakrishnan (IISWC, 2021)

Automata and Computability Education via Jove. - Ganesh Gopalakrishnan; Rick Neff (SIGCSE, 2021)

Keeping science on keel when software moves. - Dong H. Ahn; Allison H. Baker; Michael Bentley; Ian Briggs; Ganesh Gopalakrishnan; Dorit M. Hammerling; Ignacio Laguna; Gregory L. Lee; Daniel J. Milroy; Mariana Vertenstein (Commun. ACM, 2021)

Automated Dynamic Concurrency Analysis for Go. - Saeed Taheri; Ganesh Gopalakrishnan (CoRR, 2021)

Impacts of the Kuroshio Intrusion through the Luzon Strait on the Local Precipitation Anomaly. - Wen-Pin Fang; Ding-Rong Wu; Zhe-Wen Zheng; Ganesh Gopalakrishnan; Chung-Ru Ho; Quanan Zheng; Chen-Fen Huang; Hua Ho; Min-Chuan Weng (Remote. Sens., 2021)

Towards Precision-Aware Fault Tolerance Approaches for Mixed-Precision Applications. - Bo Fang 002; Siva Kumar Sastry Hari; Timothy Tsai 002; Xinyi Li; Ganesh Gopalakrishnan; Ignacio Laguna; Kevin J. Barker; Ang Li 006 (FTXS@SC, 2022)

ASAP: automatic synthesis of area-efficient and precision-aware CGRAs. - Cheng Tan 002; Thierry Tambe; Jeff Jun Zhang; Bo Fang 002; Tong Geng; Gu-Yeon Wei; David Brooks 001; Antonino Tumeo; Ganesh Gopalakrishnan; Ang Li 006 (ICS, 2022)

FPChecker: Floating-Point Exception Detection Tool and Benchmark for Parallel and Distributed HPC. - Ignacio Laguna; Tanmay Tirpankar; Xinyi Li; Ganesh Gopalakrishnan (IISWC, 2022)

An HPC Practitioner's Workbench for Formal Refinement Checking. - Juan Benavides; John W. Baugh Jr.; Ganesh Gopalakrishnan (LCPC, 2022)

BinFPE: accurate floating-point exception detection for GPU applications. - Ignacio Laguna; Xinyi Li; Ganesh Gopalakrishnan (SOAP@PLDI, 2022)

Finding Inputs that Trigger Floating-Point Exceptions in GPUs via Bayesian Optimization. - Ignacio Laguna; Ganesh Gopalakrishnan (SC, 2022)

Toward Increasing Trust in Exascale Simulations. - Dorra Ben Khalifa; Xinyi Li; Ignacio Laguna; Matthieu Martel; Ganesh Gopalakrishnan (XLOOP@SC, 2022)

Satellite observed new mechanism of Kuroshio intrusion into the northern South China Sea. - Jia-Yi Lin; Zhe-Wen Zheng; Quanan Zheng; Ding-Rong Wu; Ganesh Gopalakrishnan; Chung-Ru Ho; Jiayi Pan 001; Yu-Chun Lin; Ling-Ling Xie (Int. J. Appl. Earth Obs. Geoinformation, 2022)

Design and Evaluation of GPU-FPX: A Low-Overhead tool for Floating-Point Exception Detection in NVIDIA GPUs. - Xinyi Li; Ignacio Laguna; Bo Fang 002; Katarzyna Swirydowicz; Ang Li 006; Ganesh Gopalakrishnan (HPDC, 2023)

What Operations can be Performed Directly on Compressed Arrays, and with What Error? - Tripti Agarwal; Harvey Dam; Ponnuswamy Sadayappan; Ganesh Gopalakrishnan; Dorra Ben Khalifa; Matthieu Martel (SC Workshops, 2023)

An NSF REU Site Based on Trust and Reproducibility of Intelligent Computation: Experience Report. - Mary W. Hall; Ganesh Gopalakrishnan; Eric Eide; Johanna Cohoon; Jeff M. Phillips; Mu Zhang 001; Shireen Y. Elhabian; Aditya Bhaskara; Harvey Dam; Artem Yadrov; Tushar Kataria; Amir Mohammad Tavakkoli; et al. (SC Workshops, 2023)

Understanding the Effect of the Long Tail on Neural Network Compression. - Harvey Dam; Vinu Joseph; Aditya Bhaskara; Ganesh Gopalakrishnan; Saurav Muralidharan; Michael Garland (CoRR, 2023)

MPGemmFI: A Fault Injection Technique for Mixed Precision GEMM in ML Applications. - Bo Fang 002; Xinyi Li; Harvey Dam; Cheng Tan 002; Siva Kumar Sastry Hari; Timothy Tsai 002; Ignacio Laguna; Dingwen Tao; Ganesh Gopalakrishnan; Prashant J. Nair; Kevin J. Barker; Ang Li 006 (CoRR, 2023)

Report of the DOE/NSF Workshop on Correctness in Scientific Computing, June 2023, Orlando, FL. - Maya B. Gokhale; Ganesh Gopalakrishnan; Jackson Mayo; Santosh Nagarakatte; Cindy Rubio-González; Stephen F. Siegel (CoRR, 2023)

Finding inputs that trigger floating-point exceptions in heterogeneous computing via Bayesian optimization. - Ignacio Laguna; Anh Tran; Ganesh Gopalakrishnan (Parallel Comput., 2023)

Efficient linearizability checking for actor-based systems. - Mohammed S. Al-Mahfoudh; Ryan Stutsman; Ganesh Gopalakrishnan (Softw. Pract. Exp., 2023)

FTTN: Feature-Targeted Testing for Numerical Properties of NVIDIA & AMD Matrix Accelerators. - Xinyi Li; Ang Li 006; Bo Fang 002; Katarzyna Swirydowicz; Ignacio Laguna; Ganesh Gopalakrishnan (CCGrid, 2024)

FBTuner: A Feedback-Directed Approach for Safe Mixed-Precision Tuning. - Xinyi Li; Ganesh Gopalakrishnan (CCGrid, 2024)

Discovery of Floating-Point Differences Between NVIDIA and AMD GPUs. - Xinyi Li; Ang Li 006; Bo Fang 002; Katarzyna Swirydowicz; Ignacio Laguna; Ganesh Gopalakrishnan (CCGrid, 2024)

Understanding Mixed Precision GEMM with MPGemmFI: Insights into Fault Resilience. - Bo Fang 002; Xinyi Li; Harvey Dam; Cheng Tan 002; Siva Kumar Sastry Hari; Timothy Tsai 002; Ignacio Laguna; Dingwen Tao; Ganesh Gopalakrishnan; Prashant J. Nair; Kevin J. Barker; Ang Li 006 (CLUSTER, 2024)

FPBOXer: Efficient Input-Generation for Targeting Floating-Point Exceptions in GPU Programs. - Anh Tran; Ignacio Laguna; Ganesh Gopalakrishnan (HPDC, 2024)

SZOps: Scalar Operations for Error-bounded Lossy Compressor for Scientific Data. - Tripti Agarwal; Sheng Di; Jiajun Huang 001; Yafan Huang; Ganesh Gopalakrishnan; Robert Underwood; Kai Zhao 008; Xin Liang 001; Guanpeng Li; Franck Cappello (SC Workshops, 2024)

HiRace: Accurate and Fast Data Race Checking for GPU Programs. - John Jacobson; Martin Burtscher; Ganesh Gopalakrishnan (SC, 2024)

HiRace: Accurate and Fast Source-Level Race Checking of GPU Programs. - John Jacobson; Martin Burtscher; Ganesh Gopalakrishnan (CoRR, 2024)

A GPU accelerated mixed-precision Smoothed Particle Hydrodynamics framework with cell-based relative coordinates. - Zirui Mao; Xinyi Li; Shenyang Hu; Ganesh Gopalakrishnan; Ang Li 006 (CoRR, 2024)

Rigorous Error Analysis for Logarithmic Number Systems. - Thanh Son Nguyen; Alexey Solovyev; Ganesh Gopalakrishnan (CoRR, 2024)

FlowFPX: Nimble Tools for Debugging Floating-Point Exceptions. - Taylor Allred; Xinyi Li; Ashton Wiersdorf; Ben Greenman; Ganesh Gopalakrishnan (CoRR, 2024)

HoSZp: An Efficient Homomorphic Error-bounded Lossy Compressor for Scientific Data. - Tripti Agarwal; Sheng Di; Jiajun Huang 001; Yafan Huang; Ganesh Gopalakrishnan; Robert Underwood; Kai Zhao 008; Xin Liang 001; Guanpeng Li; Franck Cappello (CoRR, 2024)

TrackedFloats. - Taylor Allred; Xinyi Li; Ashton Wiersdorf; Ben Greenman; Ganesh Gopalakrishnan (Zenodo, 2024)

TrackedFloats. - Taylor Allred; Xinyi Li; Ashton Wiersdorf; Ben Greenman; Ganesh Gopalakrishnan (Zenodo, 2024)

Rigorous Error Analysis for Logarithmic Number Systems. - Thanh Son Nguyen; Alexey Solovyev; Mark G. Arnold; Ganesh Gopalakrishnan (ARITH, 2025)

Array Programming on GPUs: Challenges and Opportunities. - Xinyi Li; Mark Baranowski; Harvey Dam; Ganesh Gopalakrishnan (ARRAY@PLDI, 2025)

FpGuard: Static-Analysis Guided Domain Exclusions for Robust Floating-Point Error Analysis. - Tanmay Tirpankar; Artem Yadrov; Pavel Panchekha; Ganesh Gopalakrishnan (STATIC, 2025)

An SMT Formalization of Mixed-Precision Matrix Multiplication - Modeling Three Generations of Tensor Cores. - Benjamin Valpey; Xinyi Li; Sreepathi Pai; Ganesh Gopalakrishnan (NFM, 2025)

GORC: A Graph Neural Network Based Static Data Race Checker for OpenMP. - Anh Tran; Ignacio Laguna; Konstantinos Parasyris; Giorgis Georgakoudis; Ganesh Gopalakrishnan (ISC, 2025)

Equivalence Checking of a libm Port. - Mark Baranowski; Zvonimir Rakamaric; Ganesh Gopalakrishnan (TACAS (2), 2025)

Satire: Computing Rigorous Bounds for Floating-Point Rounding Error in Mixed-Precision Loop-Free Programs. - Tanmay Tirpankar; Arnab Das; Ganesh Gopalakrishnan (CoRR, 2025)

SIMT/GPU Data Race Verification using ISCC and Intermediary Code Representations: A Case Study. - Andrew Osterhout; Ganesh Gopalakrishnan (CoRR, 2025)

Directional Sign Loss: A Topology-Preserving Loss Function that Approximates the Sign of Finite Differences. - Harvey Dam; Tripti Agarwal; Ganesh Gopalakrishnan (CoRR, 2025)

Derailing Non-Answers via Logit Suppression at Output Subspace Boundaries in RLHF-Aligned Language Models. - Harvey Dam; Jonas P. Knochelmann; Vinu Joseph; Ganesh Gopalakrishnan (CoRR, 2025)