Ganesh Gopalakrishnan - researchr alias

researchr

You are not signed in
Sign in
Sign up

2011

Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. ProceedingsGanesh Gopalakrishnan, Shaz Qadeer, editors, Volume 6806 of Lecture Notes in Computer Science, Springer, 2011. [doi]

Formal specification of MPI 2.0: Case study in specifying a practical concurrent programming APIGuodong Li, Robert Palmer, Michael Delisi, Ganesh Gopalakrishnan, Robert M. Kirby. SCP, 76(2):65-81, 2011. [doi]

Formal Analysis of Message Passing - (Invited Talk)Stephen F. Siegel, Ganesh Gopalakrishnan. vmcai 2011: 2-18 [doi]

2010

Efficient methods for formally verifying safety properties of hierarchical cache coherence protocolsXiaofang Chen, Yu Yang, Ganesh Gopalakrishnan, Ching-Tsun Chou. fmsd, 36(1):37-64, 2010. [doi]

Dynamic Verification of Hybrid ProgramsWei-Fan Chiang, Grzegorz Szubzda, Ganesh Gopalakrishnan, Rajeev Thakur. pvm 2010: 298-301 [doi]

Top ten ways to make formal methods for HPC practicalGanesh Gopalakrishnan, Robert M. Kirby. FSE 2010: 137-142 [doi]

GEM: graphical explorer of MPI programsAlan Humphrey, Christopher Derrick, Ganesh Gopalakrishnan, Beth R. Tibbitts. softvis 2010: 217-218 [doi]

GEM: Graphical Explorer of MPI ProgramsAlan Humphrey, Christopher Derrick, Ganesh Gopalakrishnan, Beth Tibbitts. icppw 2010: 161-168 [doi]

A symbolic verifier for CUDA programsGuodong Li, Ganesh Gopalakrishnan, Robert M. Kirby, Dan Quinlan. ppopp 2010: 357-358 [doi]

Scalable SMT-based verification of GPU kernel functionsGuodong Li, Ganesh Gopalakrishnan. FSE 2010: 187-196 [doi]

Formal methods applied to high-performance computing software design: a case study of MPI one-sided communication-based lockingSalman Pervez, Ganesh Gopalakrishnan, Robert M. Kirby, Rajeev Thakur, William Gropp. SPE, 40(1):23-43, 2010. [doi]

Precise Dynamic Analysis for Slack Elasticity: Adding Buffering without Adding BugsSarvani S. Vakkalanka, Anh Vo, Ganesh Gopalakrishnan, Robert M. Kirby. pvm 2010: 152-159 [doi]

Scalable verification of MPI programsAnh Vo, Ganesh Gopalakrishnan. ipps 2010: 1-4 [doi]

A Scalable and Distributed Dynamic Formal Verifier for MPI ProgramsAnh Vo, Sriram Aananthakrishnan, Ganesh Gopalakrishnan, Bronis R. de Supinski, Martin Schulz, Greg Bronevetsky. sc 2010: 1-10 [doi]

Distributed dynamic partial order reductionYu Yang, Xiaofang Chen, Ganesh Gopalakrishnan, Robert M. Kirby. STTT, 12(2):113-122, 2010. [doi]

2009

How Formal Dynamic Verification Tools Facilitate Novel Concurrency VisualizationsSriram Aananthakrishnan, Michael Delisi, Sarvani S. Vakkalanka, Anh Vo, Ganesh Gopalakrishnan, Robert M. Kirby, Rajeev Thakur. pvm 2009: 261-270 [doi]

Practical Formal Verification of MPI and Thread ProgramsGanesh Gopalakrishnan, Robert M. Kirby. pvm 2009: 8 [doi]

Some resources for teaching concurrencyGanesh Gopalakrishnan, Yu Yang, Sarvani S. Vakkalanka, Anh Vo, Sriram Aananthakrishnan, Grzegorz Szubzda, Geoffrey Sawaya, Jason Williams, Subodh Sharma, Michael Delisi, Simone Atzeni. ISSTA 2009: [doi]

Proceedings of the 7th Workshop on Parallel and Distributed Systems: Testing, Analysis, and Debugging, PADTAD 2009, Chicago, Illinois, USA, July 19-20, 2009Ganesh Gopalakrishnan, Eitan Farchi, Eric Mercer, editors, ACM, 2009.

Parallel and distributed model checking in EddyIgor Melatti, Robert Palmer, Geoffrey Sawaya, Yu Yang, Robert M. Kirby, Ganesh Gopalakrishnan. STTT, 11(1):13-25, 2009. [doi]

MCC: A runtime verification tool for MCAPI user applicationsSubodh Sharma, Ganesh Gopalakrishnan, Eric Mercer, Jim Holt. FMCAD 2009: 41-44 [doi]

Reduced Execution Semantics of MPI: From Theory to PracticeSarvani S. Vakkalanka, Anh Vo, Ganesh Gopalakrishnan, Robert M. Kirby. fm 2009: 724-740 [doi]

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 2009: 329-330 [doi]

Formal verification of practical MPI programsAnh Vo, Sarvani S. Vakkalanka, Michael Delisi, Ganesh Gopalakrishnan, Robert M. Kirby, Rajeev Thakur. ppopp 2009: 261-270 [doi]

Sound and Efficient Dynamic Verification of MPI Programs with Probe Non-determinismAnh Vo, Sarvani S. Vakkalanka, Jason Williams, Ganesh Gopalakrishnan, Robert M. Kirby, Rajeev Thakur. pvm 2009: 271-281 [doi]

Automatic Discovery of Transition Symmetry in Multithreaded Programs Using Dynamic AnalysisYu Yang, Xiaofang Chen, Ganesh Gopalakrishnan, Chao Wang. spin 2009: 279-295 [doi]

2008

Runtime verification methods for MPIGanesh Gopalakrishnan, Robert M. Kirby. ipps 2008: 1-5 [doi]

Review computation engineering: applied automata theory and logicGanesh Gopalakrishnan. sigact, 39(3):30-32, 2008. [doi]

Formal specification of the MPI-2.0 standard in TLA+Guodong Li, Michael Delisi, Ganesh Gopalakrishnan, Robert M. Kirby. ppopp 2008: 283-284 [doi]

A Formal Approach to Detect Functionally Irrelevant Barriers in MPI ProgramsSubodh Sharma, Sarvani S. Vakkalanka, Ganesh Gopalakrishnan, Robert M. Kirby, Rajeev Thakur, William Gropp. pvm 2008: 265-273 [doi]

Scheduling considerations for building dynamic verification tools for MPISarvani S. Vakkalanka, Michael Delisi, Ganesh Gopalakrishnan, Robert M. Kirby. ISSTA 2008: 3 [doi]

Dynamic Verification of MPI Programs with Reductions in Presence of Split Operations and Relaxed OrderingsSarvani S. Vakkalanka, Ganesh Gopalakrishnan, Robert M. Kirby. cav 2008: 66-79 [doi]

Implementing Efficient Dynamic Formal Verification Methods for MPI ProgramsSarvani S. Vakkalanka, Michael Delisi, Ganesh Gopalakrishnan, Robert M. Kirby, Rajeev Thakur, William Gropp. pvm 2008: 248-256 [doi]

ISP: a tool for model checking MPI programsSarvani S. Vakkalanka, Subodh Sharma, Ganesh Gopalakrishnan, Robert M. Kirby. ppopp 2008: 285-286 [doi]

Dynamic Model Checking with Property Driven Pruning to Detect Race ConditionsChao Wang, Yu Yang, Aarti Gupta, Ganesh Gopalakrishnan. ATVA 2008: 126-140 [doi]

Efficient Stateful Dynamic Partial Order ReductionYu Yang, Xiaofang Chen, Ganesh Gopalakrishnan, Robert M. Kirby. spin 2008: 288-305 [doi]

2007

Transaction Based Modeling and Verification of Hardware ProtocolsXiaofang Chen, Steven M. German, Ganesh Gopalakrishnan. FMCAD 2007: 53-61 [doi]

Formal Methods for MPI ProgramsGanesh Gopalakrishnan, Robert M. Kirby. ENTCS, 193:19-27, 2007. [doi]

PrefaceGanesh Gopalakrishnan. ENTCS, 193:1-2, 2007. [doi]

PrefaceGanesh Gopalakrishnan, John O Leary. ENTCS, 174(9):1-4, 2007. [doi]

Formal Analysis for Debugging and Performance Optimization of MPIGanesh Gopalakrishnan, Robert M. Kirby. ipps 2007: 1-6 [doi]

An Approach to Formalization and Analysis of Message Passing LibrariesRobert Palmer, Michael Delisi, Ganesh Gopalakrishnan, Robert M. Kirby. fmics 2008: 164-181 [doi]

Semantics driven dynamic partial-order reduction of MPI-based parallel programsRobert Palmer, Ganesh Gopalakrishnan, Robert M. Kirby. ISSTA 2007: 43-53 [doi]

Practical Model-Checking Method for Verifying Correctness of MPI ProgramsSalman Pervez, Ganesh Gopalakrishnan, Robert M. Kirby, Robert Palmer, Rajeev Thakur, William Gropp. pvm 2007: 344-353 [doi]

Distributed Dynamic Partial Order Reduction Based Verification of Threaded SoftwareYu Yang, Xiaofang Chen, Ganesh Gopalakrishnan, Robert M. Kirby. spin 2007: 58-75 [doi]

2006

Exploiting Symmetry and Transactions for Partial Order Reduction of Rule Based SpecificationsRitwik Bhattacharya, Steven M. German, Ganesh Gopalakrishnan. spin 2006: 252-270 [doi]

Reducing Verification Complexity of a Multicore Coherence Protocol Using Assume/GuaranteeXiaofang Chen, Yu Yang, Ganesh Gopalakrishnan, Ching-Tsun Chou. FMCAD 2006: 81-88 [doi]

Computation engineering - applied automata theory and logicGanesh Gopalakrishnan. Springer, 2006. [doi]

Toward reliable and efficient message passing software through formal analysisGanesh Gopalakrishnan, Robert M. Kirby. ipps 2006: [doi]

Parallel and Distributed Model Checking in EddyIgor Melatti, Robert Palmer, Geoffrey Sawaya, Yu Yang, Robert M. Kirby, Ganesh Gopalakrishnan. spin 2006: 108-125 [doi]

Gauss: A Framework for Verifying Scientific Computing SoftwareRobert Palmer, Steve Barrus, Yu Yang, Ganesh Gopalakrishnan, Robert M. Kirby. ENTCS, 144(3):95-106, 2006. [doi]

Formal Verification of Programs That Use MPI One-Sided CommunicationSalman Pervez, Ganesh Gopalakrishnan, Robert M. Kirby, Rajeev Thakur, William D. Gropp. pvm 2006: 30-39 [doi]

2005

Symbolic Partial Order Reduction for Rule Based Transition SystemsRitwik Bhattacharya, Steven M. German, Ganesh Gopalakrishnan. charme 2005: 332-335 [doi]

Live sequence charts applied to hardware requirements specification and verificationAnnette Bunker, Ganesh Gopalakrishnan, Konrad Slind. STTT, 7(4):341-350, 2005. [doi]

Counterexample Guided Invariant Discovery for Parameterized Cache Coherence VerificationSudhindra Pandav, Konrad Slind, Ganesh Gopalakrishnan. charme 2005: 317-331 [doi]

On the definition of sequential consistencyAli Sezgin, Ganesh Gopalakrishnan. ipl, 96(6):193-196, 2005. [doi]

On the decidability of shared memory consistency verificationAli Sezgin, Ganesh Gopalakrishnan. memocode 2005: 199-208 [doi]

UMM: an operational memory model specification framework with integrated model checking capabilityYue Yang, Ganesh Gopalakrishnan, Gary Lindstrom. concurrency, 17(5-6):465-487, 2005. [doi]

2004

Formal hardware specification languages for protocol compliance verificationAnnette Bunker, Ganesh Gopalakrishnan, Sally A. McKee. todaes, 9(1):1-32, 2004. [doi]

QB or Not QB: An Efficient Execution Verification Tool for Memory OrderingsGanesh Gopalakrishnan, Yue Yang, Hemanthkumar Sivaraj. cav 2004: 401-413 [doi]

Theorem Proving in Higher Order Logics, 17th International Conference, TPHOLs 2004, Park City, Utah, USA, September 14-17, 2004, ProceedingsKonrad Slind, Annette Bunker, Ganesh Gopalakrishnan, editors, Volume 3223 of Lecture Notes in Computer Science, Springer, 2004.

Nemos: A Framework for Axiomatic and Executable Specifications of Memory Consistency ModelsYue Yang, Ganesh Gopalakrishnan, Gary Lindstrom, Konrad Slind. ipps 2004: [doi]

Memory-Model-Sensitive Data Race AnalysisYue Yang, Ganesh Gopalakrishnan, Gary Lindstrom. icfem 2004: 30-45 [doi]

2003

2002

Incremental Proof of the Producer/Consumer Property for the PCI ProtocolDominique Cansell, Ganesh Gopalakrishnan, Michael D. Jones, Dominique Méry, Airy Weinzoepflen. zum 2002: 22-41 [doi]

A Specification and Verification Framework for Developing Weak Shared Memory Consistency ProtocolsProsenjit Chatterjee, Ganesh Gopalakrishnan. FMCAD 2002: 292-309 [doi]

Shared Memory Consistency Protocol Verification Against Weak Memory Models: Refinement via Model-CheckingProsenjit Chatterjee, Hemanthkumar Sivaraj, Ganesh Gopalakrishnan. cav 2002: 123-136 [doi]

Robust rate based congestion controlGanesh Gopalakrishnan, Sneha Kumar Kasera. ccr, 32(3):22, 2002. [doi]

An Efficient Partial Order Reduction Algorithm with an Alternative Proviso ImplementationRatan Nalumasu, Ganesh Gopalakrishnan. fmsd, 20(3):231-247, 2002.

Deriving Efficient Cache Coherence Protocols Through RefinementRatan Nalumasu, Ganesh Gopalakrishnan. fmsd, 20(1):107-125, 2002.

A Distributed Partial Order Reduction AlgorithmRobert Palmer, Ganesh Gopalakrishnan. forte 2002: 370 [doi]

Specifying Java thread semantics using a uniform memory modelYue Yang, Ganesh Gopalakrishnan, Gary Lindstrom. java 2002: 192-201 [doi]

2001

towards A formal Model of Shared Memory Consistency for Intel Itanium:::TM:::Prosenjit Chatterjee, Ganesh Gopalakrishnan. iccd 2001: 515-518

2000

Verification Methods for Weaker Shared Memory Consistency ModelsRajnish Ghughal, Ganesh Gopalakrishnan. ipps 2000: 985-992 [doi]

Introduction: Formal Methods for CAD: Enabling Technologies and System-level ApplicationsGanesh Gopalakrishnan. fmsd, 16(1):5-6, 2000.

Verifying Advanced Microarchitectures that Support Speculation and ExceptionsRavi Hosabettu, Ganesh Gopalakrishnan, Mandayam K. Srivas. cav 2000: 521-537

Achieving Fast and Exact Hazard-Free Logic Minimization of Extended Burst-Mode gC Finite State MachinesHans M. Jacobson, Chris J. Myers, Ganesh Gopalakrishnan. iccad 2000: 303-310

High-Level Asynchronous System Design Using the ACK FrameworkHans M. Jacobson, Erik Brunvand, Ganesh Gopalakrishnan, Prabhakar Kudva. async 2000: 93-103 [doi]

Verifying Transaction Ordering Properties in Unbounded Bus Networks through Combined Deductive/Algorithmic MethodsMichael D. Jones, Ganesh Gopalakrishnan. FMCAD 2000: 505-519 [doi]

Formalization and Analysis of a Solution to the PCI 2.1 Bus Transaction Ordering ProblemAbdel Mokkedem, Ravi Hosabettu, Michael D. Jones, Ganesh Gopalakrishnan. fmsd, 16(1):93-119, 2000.

1999

Peephole optimization of asynchronous macromodule networksGanesh Gopalakrishnan, Prabhakar Kudva, Erik Brunvand. tvlsi, 7(1):30-37, 1999. [doi]

A Proof of Correctness of a Processor Implementing Tomasulo s Algorithm without a Reorder BufferRavi Hosabettu, Ganesh Gopalakrishnan, Mandayam K. Srivas. charme 1999: 8-22 [doi]

Timing constraints for high-speed counterflow-clocked pipeliningJae-Tack Yoo, Ganesh Gopalakrishnan, Kent F. Smith. tvlsi, 7(2):167-173, 1999. [doi]

1998

Using Test Model-Checking to Verify the Runway-PA8000 Memory ModelRajnish Ghughal, Abdelillah Mokkedem, Ratan Nalumasu, Ganesh Gopalakrishnan. spaa 1998: 231-239 [doi]

Formal Methods in Computer-Aided Design, Second International Conference, FMCAD 98, Palo Alto, California, USA, November 4-6, 1998, ProceedingsGanesh Gopalakrishnan, Phillip J. Windley, editors, Volume 1522 of Lecture Notes in Computer Science, Springer, 1998.

Decomposing the Proof of Correctness of pipelined MicroprocessorsRavi Hosabettu, Mandayam K. Srivas, Ganesh Gopalakrishnan. cav 1998: 122-134

Formalization and Proof of a Solution to the PCI 2.1 Bus Transaction Ordering ProblemAbdelillah Mokkedem, Ravi Hosabettu, Ganesh Gopalakrishnan. FMCAD 1998: 237-254 [doi]

Deriving Efficient Cache Coherence Protocols through RefinementRatan Nalumasu, Ganesh Gopalakrishnan. ipps 1998: 857-870

PV: An Explicit Enumeration Model-CheckerRatan Nalumasu, Ganesh Gopalakrishnan. FMCAD 1998: 523-528 [doi]

The Test Model-Checking Approach to the Verification of Formal Memory Models of MultiprocessorsRatan Nalumasu, Rajnish Ghughal, Abdelillah Mokkedem, Ganesh Gopalakrishnan. cav 1998: 464-476

1997

Formal modeling and validation applied to a commercial coherent bus: a case studyGanesh Gopalakrishnan, Rajnish Ghughal, Ravi Hosabettu, Abdelillah Mokkedem, Ratan Nalumasu. charme 1997: 48-62

Asynchronous Microengines for Efficient High-level ControlHans M. Jacobson, Ganesh Gopalakrishnan. arvlsi 1997: 201-218 [doi]

1996

Synthesis for Hazard-free Customized CMOS Complex-Gate Networks Under Multiple-Input ChangesPrabhakar Kudva, Ganesh Gopalakrishnan, Hans M. Jacobson, Steven M. Nowick. dac 1996: 77-82 [doi]

A Technique for Synthesizing Distributed Burst-mode CircuitsPrabhakar Kudva, Ganesh Gopalakrishnan, Hans M. Jacobson. dac 1996: 67-70 [doi]

1995

High speed counterflow-clocked pipelining illustrated on the design of HDTV subband vector quantizer chipsJae-Tack Yoo, Ganesh Gopalakrishnan, Kent F. Smith, V. John Mathews. arvlsi 1995: 91-107 [doi]

1994

Developing Micropipeline Wavefront ArbitersGanesh Gopalakrishnan. dt, 11(4):55-64, 1994. [doi]

PreviousNext