Person: Ganesh Gopalakrishnan

DBLP: Gopalakrishnan:Ganesh

Facilitated 1 volumes:

Ed

Contributed to:

2015

2015

2014

2012

2011

2010

2010

2010

2009

2009

2008

2008

2004

2002

2000

1998

1996

1992

2016

2017

Wrote 23 papers:

ASPLOS-2015-AlglaveBDGKPSW #behaviour #concurrent #gpu #programming

GPU Concurrency: Weak Behaviours and Programming Assumptions (JA, MB, AFD, GG, JK, DP, TS, JW), pp. 577–591.

FM-2015-SolovyevJRG #estimation #fault #float

Rigorous Estimation of Floating-Point Round-off Errors with Symbolic Taylor Expansions (AS, CJ, ZR, GG), pp. 532–550.

PPoPP-2014-ChiangGRS #fault #float #performance

Efficient search for inputs causing high floating-point errors (WFC, GG, ZR, AS), pp. 43–52.

PPoPP-2012-LiLSGGR #generative #named #testing #verification

GKLEE: concolic verification and test generation for GPUs (GL, PL, GS, GG, IG, SPR), pp. 215–224.

VMCAI-2011-SiegelG #analysis #formal method #message passing

Formal Analysis of Message Passing — (SFS, GG), pp. 2–18.

FSE-2010-LiG #gpu #kernel #scalability #smt #verification

Scalable SMT-based verification of GPU kernel functions (GL, GG), pp. 187–196.

PPoPP-2010-LiGKQ #source code #verification

A symbolic verifier for CUDA programs (GL, GG, RMK, DQ), pp. 357–358.

SOFTVIS-2010-HumphreyDGT #named #source code #visual notation

GEM: graphical explorer of MPI programs (AH, CD, GG, BRT), pp. 217–218.

FM-2009-VakkalankaVGK #execution #semantics #theory and practice

Reduced Execution Semantics of MPI: From Theory to Practice (SSV, AV, GG, RMK), pp. 724–740.

PPoPP-2009-VoVDGKT #source code #verification

Formal verification of practical MPI programs (AV, SSV, MD, GG, RMK, RT), pp. 261–270.

CAV-2008-VakkalankaGK #order #reduction #source code #verification

Dynamic Verification of MPI Programs with Reductions in Presence of Split Operations and Relaxed Orderings (SSV, GG, RMK), pp. 66–79.

PPoPP-2008-LiDGK #specification #standard

Formal specification of the MPI-2.0 standard in TLA+ (GL, MD, GG, RMK), pp. 283–284.

PPoPP-2008-VakkalankaSGK #model checking #named #source code

ISP: a tool for model checking MPI programs (SSV, SS, GG, RMK), pp. 285–286.

CAV-2004-GopalakrishnanYS #execution #memory management #order #performance #verification

QB or Not QB: An Efficient Execution Verification Tool for Memory Orderings (GG, YY, HS), pp. 401–413.

CAV-2002-ChatterjeeSG #consistency #memory management #model checking #modelling #protocol #refinement #verification

Shared Memory Consistency Protocol Verification Against Weak Memory Models: Refinement via Model-Checking (PC, HS, GG), pp. 123–136.

CAV-2000-HosabettuGS #architecture #exception #verification

Verifying Advanced Microarchitectures that Support Speculation and Exceptions (RH, GG, MKS), pp. 521–537.

CAV-1998-HosabettuSG #correctness #pipes and filters #proving

Decomposing the Proof of Correctness of pipelined Microprocessors (RH, MKS, GG), pp. 122–134.

CAV-1998-NalumasuGMG #approach #memory management #model checking #modelling #multi #verification

The “Test Model-Checking” Approach to the Verification of Formal Memory Models of Multiprocessors (RN, RG, AM, GG), pp. 464–476.

DAC-1996-KudvaGJ #distributed

A Technique for Synthesizing Distributed Burst-mode Circuits (PK, GG, HMJ), pp. 67–70.

DAC-1996-KudvaGJN #multi #network #synthesis

Synthesis for Hazard-free Customized CMOS Complex-Gate Networks Under Multiple-Input Changes (PK, GG, HMJ, SMN), pp. 77–82.

CAV-1992-JainKG #scalability #towards #verification

Towards a Verification Technique for Large Synchronous Circuits (PJ, PK, GG), pp. 109–122.

OOPSLA-2016-SorensenDBGR

Portable inter-workgroup barrier synchronisation for GPUs (TS0, AFD, MB, GG, ZR), pp. 39–58.

POPL-2017-ChiangBBSGR #float

Rigorous floating-point mixed-precision tuning (WFC, MB, IB, AS, GG, ZR), pp. 300–315.