BibSLEIGH
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
Travelled to:
1 × Denmark
1 × India
1 × Norway
1 × The Netherlands
1 × Turkey
11 × USA
2 × Canada
Collaborated with:
R.M.Kirby G.Li S.S.Vakkalanka P.Kudva Z.Rakamaric A.Solovyev H.Sivaraj R.Hosabettu M.K.Srivas H.M.Jacobson S.F.Siegel W.Chiang A.Vo M.Delisi Y.Yang P.Chatterjee P.Jain M.Batty A.F.Donaldson C.Jacobsen D.Quinlan A.Humphrey C.Derrick B.R.Tibbitts S.Sharma R.Nalumasu R.Ghughal A.Mokkedem S.M.Nowick T.S.0001 P.Li G.Sawaya I.Ghosh S.P.Rajan R.Thakur Mark Baranowski Ian Briggs J.Alglave J.Ketema D.Pötzl T.Sorensen J.Wickerson
Talks about:
verif (8) program (6) mpi (6) model (5) memori (4) formal (4) point (3) float (3) check (3) techniqu (2)

Person: Ganesh Gopalakrishnan

DBLP DBLP: Gopalakrishnan:Ganesh

Facilitated 1 volumes:

CAV 2011Ed

Contributed to:

ASPLOS 20152015
FM 20152015
PPoPP 20142014
PPoPP 20122012
VMCAI 20112011
FSE 20102010
PPoPP 20102010
SOFTVIS 20102010
FM 20092009
PPoPP 20092009
CAV 20082008
PPoPP 20082008
CAV 20042004
CAV 20022002
CAV 20002000
CAV 19981998
DAC 19961996
CAV 19921992
OOPSLA 20162016
POPL 20172017

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.

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.