| 2009 | ||
|---|---|---|
| 100 | Sarvani S. Vakkalanka, Anh Vo, Ganesh Gopalakrishnan, Robert M. Kirby: Reduced Execution Semantics of MPI: From Theory to Practice. FM 2009: 724-740 | |
| 99 | Anh Vo, Sarvani S. Vakkalanka, Michael Delisi, Ganesh Gopalakrishnan, Robert M. Kirby, Rajeev Thakur: Formal verification of practical MPI programs. PPOPP 2009: 261-270 | |
| 98 | Sriram Aananthakrishnan, Michael Delisi, Sarvani S. Vakkalanka, Anh Vo, Ganesh Gopalakrishnan, Robert M. Kirby, Rajeev Thakur: How Formal Dynamic Verification Tools Facilitate Novel Concurrency Visualizations. PVM/MPI 2009: 261-270 | |
| 97 | Anh Vo, Sarvani S. Vakkalanka, Jason Williams, Ganesh Gopalakrishnan, Robert M. Kirby, Rajeev Thakur: Sound and Efficient Dynamic Verification of MPI Programs with Probe Non-determinism. PVM/MPI 2009: 271-281 | |
| 96 | Sarvani S. Vakkalanka, Grzegorz Szubzda, Anh Vo, Ganesh Gopalakrishnan, Robert M. Kirby, Rajeev Thakur: Static-Analysis Assisted Dynamic Verification of MPI Waitany Programs (Poster Abstract). PVM/MPI 2009: 329-330 | |
| 95 | Ganesh Gopalakrishnan, Robert M. Kirby: Practical Formal Verification of MPI and Thread Programs. PVM/MPI 2009: 8 | |
| 94 | Yu Yang, Xiaofang Chen, Ganesh Gopalakrishnan, Chao Wang: Automatic Discovery of Transition Symmetry in Multithreaded Programs Using Dynamic Analysis. SPIN 2009: 279-295 | |
| 93 | Igor Melatti, Robert Palmer, Geoffrey Sawaya, Yu Yang, Robert M. Kirby, Ganesh Gopalakrishnan: Parallel and distributed model checking in Eddy. STTT 11(1): 13-25 (2009) | |
| 2008 | ||
| 92 | Chao Wang, Yu Yang, Aarti Gupta, Ganesh Gopalakrishnan: Dynamic Model Checking with Property Driven Pruning to Detect Race Conditions. ATVA 2008: 126-140 | |
| 91 | Sarvani S. Vakkalanka, Ganesh Gopalakrishnan, Robert M. Kirby: Dynamic Verification of MPI Programs with Reductions in Presence of Split Operations and Relaxed Orderings. CAV 2008: 66-79 | |
| 90 | Ganesh Gopalakrishnan, Robert M. Kirby: Runtime verification methods for MPI. IPDPS 2008: 1-5 | |
| 89 | Sarvani S. Vakkalanka, Michael Delisi, Ganesh Gopalakrishnan, Robert M. Kirby: Scheduling considerations for building dynamic verification tools for MPI. PADTAD 2008: 3 | |
| 88 | Guodong Li, Michael Delisi, Ganesh Gopalakrishnan, Robert M. Kirby: Formal specification of the MPI-2.0 standard in TLA+. PPOPP 2008: 283-284 | |
| 87 | Sarvani S. Vakkalanka, Subodh Sharma, Ganesh Gopalakrishnan, Robert M. Kirby: ISP: a tool for model checking MPI programs. PPOPP 2008: 285-286 | |
| 86 | Sarvani S. Vakkalanka, Michael Delisi, Ganesh Gopalakrishnan, Robert M. Kirby, Rajeev Thakur, William Gropp: Implementing Efficient Dynamic Formal Verification Methods for MPI Programs. PVM/MPI 2008: 248-256 | |
| 85 | Subodh Sharma, Sarvani S. Vakkalanka, Ganesh Gopalakrishnan, Robert M. Kirby, Rajeev Thakur, William Gropp: A Formal Approach to Detect Functionally Irrelevant Barriers in MPI Programs. PVM/MPI 2008: 265-273 | |
| 84 | Yu Yang, Xiaofang Chen, Ganesh Gopalakrishnan, Robert M. Kirby: Efficient Stateful Dynamic Partial Order Reduction. SPIN 2008: 288-305 | |
| 83 | Ganesh Gopalakrishnan: Review computation engineering: applied automata theory and logic. SIGACT News 39(3): 30-32 (2008) | |
| 2007 | ||
| 82 | Xiaofang Chen, Steven M. German, Ganesh Gopalakrishnan: Transaction Based Modeling and Verification of Hardware Protocols. FMCAD 2007: 53-61 | |
| 81 | Robert Palmer, Michael Delisi, Ganesh Gopalakrishnan, Robert M. Kirby: An Approach to Formalization and Analysis of Message Passing Libraries. FMICS 2007: 164-181 | |
| 80 | Ganesh Gopalakrishnan, Robert M. Kirby: Formal Analysis for Debugging and Performance Optimization of MPI. IPDPS 2007: 1-6 | |
| 79 | Robert Palmer, Ganesh Gopalakrishnan, Robert M. Kirby: Semantics driven dynamic partial-order reduction of MPI-based parallel programs. PADTAD 2007: 43-53 | |
| 78 | Salman Pervez, Ganesh Gopalakrishnan, Robert M. Kirby, Robert Palmer, Rajeev Thakur, William Gropp: Practical Model-Checking Method for Verifying Correctness of MPI Programs. PVM/MPI 2007: 344-353 | |
| 77 | Yu Yang, Xiaofang Chen, Ganesh Gopalakrishnan, Robert M. Kirby: Distributed Dynamic Partial Order Reduction Based Verification of Threaded Software. SPIN 2007: 58-75 | |
| 76 | Ganesh Gopalakrishnan, John O'Leary: Preface. Electr. Notes Theor. Comput. Sci. 174(9): 1-4 (2007) | |
| 75 | Ganesh Gopalakrishnan: Preface. Electr. Notes Theor. Comput. Sci. 193: 1-2 (2007) | |
| 74 | Ganesh Gopalakrishnan, Robert M. Kirby: Formal Methods for MPI Programs. Electr. Notes Theor. Comput. Sci. 193: 19-27 (2007) | |
| 2006 | ||
| 73 | Xiaofang Chen, Yu Yang, Ganesh Gopalakrishnan, Ching-Tsun Chou: Reducing Verification Complexity of a Multicore Coherence Protocol Using Assume/Guarantee. FMCAD 2006: 81-88 | |
| 72 | Ganesh Gopalakrishnan, Robert M. Kirby: Toward reliable and efficient message passing software through formal analysis. IPDPS 2006 | |
| 71 | Salman Pervez, Ganesh Gopalakrishnan, Robert M. Kirby, Rajeev Thakur, William D. Gropp: Formal Verification of Programs That Use MPI One-Sided Communication. PVM/MPI 2006: 30-39 | |
| 70 | Igor Melatti, Robert Palmer, Geoffrey Sawaya, Yu Yang, Robert M. Kirby, Ganesh Gopalakrishnan: Parallel and Distributed Model Checking in Eddy. SPIN 2006: 108-125 | |
| 69 | Ritwik Bhattacharya, Steven M. German, Ganesh Gopalakrishnan: Exploiting Symmetry and Transactions for Partial Order Reduction of Rule Based Specifications. SPIN 2006: 252-270 | |
| 68 | Robert Palmer, Steve Barrus, Yu Yang, Ganesh Gopalakrishnan, Robert M. Kirby: Gauss: A Framework for Verifying Scientific Computing Software. Electr. Notes Theor. Comput. Sci. 144(3): 95-106 (2006) | |
| 2005 | ||
| 67 | Sudhindra Pandav, Konrad Slind, Ganesh Gopalakrishnan: Counterexample Guided Invariant Discovery for Parameterized Cache Coherence Verification. CHARME 2005: 317-331 | |
| 66 | Ritwik Bhattacharya, Steven M. German, Ganesh Gopalakrishnan: Symbolic Partial Order Reduction for Rule Based Transition Systems. CHARME 2005: 332-335 | |
| 65 | Ali Sezgin, Ganesh Gopalakrishnan: On the decidability of shared memory consistency verification. MEMOCODE 2005: 199-208 | |
| 64 | Yue Yang, Ganesh Gopalakrishnan, Gary Lindstrom: UMM: an operational memory model specification framework with integrated model checking capability. Concurrency - Practice and Experience 17(5-6): 465-487 (2005) | |
| 63 | Ali Sezgin, Ganesh Gopalakrishnan: On the definition of sequential consistency. Inf. Process. Lett. 96(6): 193-196 (2005) | |
| 62 | Annette Bunker, Ganesh Gopalakrishnan, Konrad Slind: Live sequence charts applied to hardware requirements specification and verification. STTT 7(4): 341-350 (2005) | |
| 2004 | ||
| 61 | Konrad Slind, Annette Bunker, Ganesh Gopalakrishnan: Theorem Proving in Higher Order Logics, 17th International Conference, TPHOLs 2004, Park City, Utah, USA, September 14-17, 2004, Proceedings Springer 2004 | |
| 60 | Ganesh Gopalakrishnan, Yue Yang, Hemanthkumar Sivaraj: QB or Not QB: An Efficient Execution Verification Tool for Memory Orderings. CAV 2004: 401-413 | |
| 59 | Yue Yang, Ganesh Gopalakrishnan, Gary Lindstrom: Memory-Model-Sensitive Data Race Analysis. ICFEM 2004: 30-45 | |
| 58 | Yue Yang, Ganesh Gopalakrishnan, Gary Lindstrom, Konrad Slind: Nemos: A Framework for Axiomatic and Executable Specifications of Memory Consistency Models. IPDPS 2004 | |
| 57 | Annette Bunker, Ganesh Gopalakrishnan, Sally A. McKee: Formal hardware specification languages for protocol compliance verification. ACM Trans. Design Autom. Electr. Syst. 9(1): 1-32 (2004) | |
| 2003 | ||
| 56 | Yue Yang, Ganesh Gopalakrishnan, Gary Lindstrom, Konrad Slind: Analyzing the Intel Itanium Memory Ordering Rules Using Logic Programming and SAT. CHARME 2003: 81-95 | |
| 55 | Hemanthkumar Sivaraj, Ganesh Gopalakrishnan: Random Walk Based Heuristic Algorithms for Distributed Memory Model Checking. Electr. Notes Theor. Comput. Sci. 89(1): (2003) | |
| 54 | Ganesh Gopalakrishnan, Warren A. Hunt Jr.: Industrial Practice of Formal Hardware Verification: A Sampling. Formal Methods in System Design 22(2): 95-99 (2003) | |
| 53 | Ravi Hosabettu, Ganesh Gopalakrishnan, Mandayam K. Srivas: Formal Verification of a Complex Pipelined Processor. Formal Methods in System Design 23(2): 171-213 (2003) | |
| 52 | Ravi Hosabettu, Ganesh Gopalakrishnan, Mandayam K. Srivas: A Practical Methodology for Verifying Pipelined Microarchitectures. IEEE Design & Test of Computers 20(4): 4-14 (2003) | |
| 2002 | ||
| 51 | Prosenjit Chatterjee, Hemanthkumar Sivaraj, Ganesh Gopalakrishnan: Shared Memory Consistency Protocol Verification Against Weak Memory Models: Refinement via Model-Checking. CAV 2002: 123-136 | |
| 50 | Prosenjit Chatterjee, Ganesh Gopalakrishnan: A Specification and Verification Framework for Developing Weak Shared Memory Consistency Protocols. FMCAD 2002: 292-309 | |
| 49 | Robert Palmer, Ganesh Gopalakrishnan: A Distributed Partial Order Reduction Algorithm. FORTE 2002: 370 | |
| 48 | Yue Yang, Ganesh Gopalakrishnan, Gary Lindstrom: Specifying Java thread semantics using a uniform memory model. Java Grande 2002: 192-201 | |
| 47 | Dominique Cansell, Ganesh Gopalakrishnan, Michael D. Jones, Dominique Méry, Airy Weinzoepflen: Incremental Proof of the Producer/Consumer Property for the PCI Protocol. ZB 2002: 22-41 | |
| 46 | Ganesh Gopalakrishnan, Sneha Kumar Kasera: Robust rate based congestion control. Computer Communication Review 32(3): 22 (2002) | |
| 45 | Ratan Nalumasu, Ganesh Gopalakrishnan: Deriving Efficient Cache Coherence Protocols Through Refinement. Formal Methods in System Design 20(1): 107-125 (2002) | |
| 44 | Ratan Nalumasu, Ganesh Gopalakrishnan: An Efficient Partial Order Reduction Algorithm with an Alternative Proviso Implementation. Formal Methods in System Design 20(3): 231-247 (2002) | |
| 2001 | ||
| 43 | Prosenjit Chatterjee, Ganesh Gopalakrishnan: towards A formal Model of Shared Memory Consistency for Intel ItaniumTM. ICCD 2001: 515-518 | |
| 2000 | ||
| 42 | Hans M. Jacobson, Erik Brunvand, Ganesh Gopalakrishnan, Prabhakar Kudva: High-Level Asynchronous System Design Using the ACK Framework. ASYNC 2000: 93-103 | |
| 41 | Ravi Hosabettu, Ganesh Gopalakrishnan, Mandayam K. Srivas: Verifying Advanced Microarchitectures that Support Speculation and Exceptions. CAV 2000: 521-537 | |
| 40 | Michael D. Jones, Ganesh Gopalakrishnan: Verifying Transaction Ordering Properties in Unbounded Bus Networks through Combined Deductive/Algorithmic Methods. FMCAD 2000: 505-519 | |
| 39 | Hans M. Jacobson, Chris J. Myers, Ganesh Gopalakrishnan: Achieving Fast and Exact Hazard-Free Logic Minimization of Extended Burst-Mode gC Finite State Machines. ICCAD 2000: 303-310 | |
| 38 | Rajnish Ghughal, Ganesh Gopalakrishnan: Verification Methods for Weaker Shared Memory Consistency Models. IPDPS Workshops 2000: 985-992 | |
| 37 | Ganesh Gopalakrishnan: Introduction: Formal Methods for CAD: Enabling Technologies and System-level Applications. Formal Methods in System Design 16(1): 5-6 (2000) | |
| 36 | Abdel Mokkedem, Ravi Hosabettu, Michael D. Jones, Ganesh Gopalakrishnan: Formalization and Analysis of a Solution to the PCI 2.1 Bus Transaction Ordering Problem. Formal Methods in System Design 16(1): 93-119 (2000) | |
| 1999 | ||
| 35 | Ravi Hosabettu, Ganesh Gopalakrishnan, Mandayam K. Srivas: A Proof of Correctness of a Processor Implementing Tomasulo's Algorithm without a Reorder Buffer. CHARME 1999: 8-22 | |
| 34 | Ganesh Gopalakrishnan, Prabhakar Kudva, Erik Brunvand: Peephole optimization of asynchronous macromodule networks. IEEE Trans. VLSI Syst. 7(1): 30-37 (1999) | |
| 33 | Jae-Tack Yoo, Ganesh Gopalakrishnan, Kent F. Smith: Timing constraints for high-speed counterflow-clocked pipelining. IEEE Trans. VLSI Syst. 7(2): 167-173 (1999) | |
| 1998 | ||
| 32 | Ganesh Gopalakrishnan, Phillip J. Windley: Formal Methods in Computer-Aided Design, Second International Conference, FMCAD '98, Palo Alto, California, USA, November 4-6, 1998, Proceedings Springer 1998 | |
| 31 | Ravi Hosabettu, Mandayam K. Srivas, Ganesh Gopalakrishnan: Decomposing the Proof of Correctness of pipelined Microprocessors. CAV 1998: 122-134 | |
| 30 | Ratan Nalumasu, Rajnish Ghughal, Abdelillah Mokkedem, Ganesh Gopalakrishnan: The 'Test Model-Checking' Approach to the Verification of Formal Memory Models of Multiprocessors. CAV 1998: 464-476 | |
| 29 | Abdelillah Mokkedem, Ravi Hosabettu, Ganesh Gopalakrishnan: Formalization and Proof of a Solution to the PCI 2.1 Bus Transaction Ordering Problem. FMCAD 1998: 237-254 | |
| 28 | Ratan Nalumasu, Ganesh Gopalakrishnan: PV: An Explicit Enumeration Model-Checker. FMCAD 1998: 523-528 | |
| 27 | Ratan Nalumasu, Ganesh Gopalakrishnan: Deriving Efficient Cache Coherence Protocols through Refinement. IPPS/SPDP Workshops 1998: 857-870 | |
| 26 | Rajnish Ghughal, Abdelillah Mokkedem, Ratan Nalumasu, Ganesh Gopalakrishnan: Using "Test Model-Checking" to Verify the Runway-PA8000 Memory Model. SPAA 1998: 231-239 | |
| 1997 | ||
| 25 | Hans M. Jacobson, Ganesh Gopalakrishnan: Asynchronous Microengines for Efficient High-level Control. ARVLSI 1997: 201-218 | |
| 24 | Ganesh Gopalakrishnan, Rajnish Ghughal, Ravi Hosabettu, Abdelillah Mokkedem, Ratan Nalumasu: Formal modeling and validation applied to a commercial coherent bus: a case study. CHARME 1997: 48-62 | |
| 1996 | ||
| 23 | Prabhakar Kudva, Ganesh Gopalakrishnan, Hans M. Jacobson: A Technique for Synthesizing Distributed Burst-mode Circuits. DAC 1996: 67-70 | |
| 22 | Prabhakar Kudva, Ganesh Gopalakrishnan, Hans M. Jacobson, Steven M. Nowick: Synthesis for Hazard-free Customized CMOS Complex-Gate Networks Under Multiple-Input Changes. DAC 1996: 77-82 | |
| 1995 | ||
| 21 | Jae-Tack Yoo, Ganesh Gopalakrishnan, Kent F. Smith, V. John Mathews: High speed counterflow-clocked pipelining illustrated on the design of HDTV subband vector quantizer chips. ARVLSI 1995: 91-107 | |
| 1994 | ||
| 20 | Prabhakar Kudva, Ganesh Gopalakrishnan, Erik Brunvand, Venkatesh Akella: Performance Analysis and Optimization of Asynchronous Circuits. ICCD 1994: 221-224 | |
| 19 | Ganesh Gopalakrishnan, Prabhakar Kudva, Erik Brunvand: Peephole Optimization of Asynchronous Macromodule Networks. ICCD 1994: 442-446 | |
| 18 | Ganesh Gopalakrishnan: Developing Micropipeline Wavefront Arbiters. IEEE Design & Test of Computers 11(4): 55-64 (1994) | |
| 17 | Venkatesh Akella, Ganesh Gopalakrishnan: Specification and Validation of Control-Intensive IC's in hopCP. IEEE Trans. Software Eng. 20(6): 405-423 (1994) | |
| 16 | Ganesh Gopalakrishnan, Erik Brunvand, Nick Michell, Steven M. Nowick: A correctness criterion for asynchronous circuit validation and optimization. IEEE Trans. on CAD of Integrated Circuits and Systems 13(11): 1309-1318 (1994) | |
| 15 | Prabhat Jain, Ganesh Gopalakrishnan: Efficient symbolic simulation-based verification using the parametric form of Boolean expressions. IEEE Trans. on CAD of Integrated Circuits and Systems 13(8): 1005-1015 (1994) | |
| 14 | Venkatesh Akella, Ganesh Gopalakrishnan: CFSIM: A Concurrent Compiled Code Functional Simulator for hopCP. Int. Journal in Computer Simulation 4(4): 0- (1994) | |
| 13 | Ganesh Gopalakrishnan, Venkatesh Akella: High-level optimizations in compiling process descriptions to asynchronous circuits. VLSI Signal Processing 7(1-2): 33-45 (1994) | |
| 1993 | ||
| 12 | Prabhat Jain, Ganesh Gopalakrishnan: Hierarchical Constraint Solving in the Parametric Form with Applications to Efficient Symbolic Simulation Based Verification. ICCD 1993: 304-307 | |
| 11 | Ganesh Gopalakrishnan, Venkatesh Akella: A transformational approach to asynchronous high-level synthesis. VLSI 1993: 201-210 | |
| 10 | Ganesh Gopalakrishnan, Richard Fujimoto: Design and Verification of the Rollback Chip Using HOP: A Case Study of Formal Methods Applied to Hardware design. ACM Trans. Comput. Syst. 11(2): 109-145 (1993) | |
| 1992 | ||
| 9 | Prabhat Jain, Prabhakar Kudva, Ganesh Gopalakrishnan: Towards a Verification Technique for Large Synchronous Circuits. CAV 1992: 109-122 | |
| 8 | Venkatesh Akella, Ganesh Gopalakrishnan: SHILPA: a high-level synthesis system for self-timed circuits. ICCAD 1992: 587-591 | |
| 7 | Armin Liebchen, Ganesh Gopalakrishnan: Dynamic Reordering of Hgh Latency Transactions Using a Modified a Micropipeline. ICCD 1992: 336-340 | |
| 6 | Prabhat Jain, Ganesh Gopalakrishnan: Some Techniques for Efficient Symbolic Simulation-Based Verification. ICCD 1992: 598-602 | |
| 5 | Richard Fujimoto, Jya-Jang Tsai, Ganesh Gopalakrishnan: Design and Evaluation of the Rollback Chip: Special Purpose Hardware for Time Warp. IEEE Trans. Computers 41(1): 68-82 (1992) | |
| 1989 | ||
| 4 | Ganesh Gopalakrishnan, Narayana Mani, Venkatesh Akella: Parallel Composition of Lockstep Synchronous Processes for Hardware Validation: Divide-and-Conquer Composition. Automatic Verification Methods for Finite State Systems 1989: 374-382 | |
| 1988 | ||
| 3 | Richard Fujimoto, Jya-Jang Tsai, Ganesh Gopalakrishnan: Design and Performance of Special Purpose Hardware for Time Warp. ISCA 1988: 401-408 | |
| 2 | Ganesh Gopalakrishnan, Mandayam K. Srivas: Implementing Functional Programs Using Mutable Abstract Data Types. Inf. Process. Lett. 26(6): 277-286 (1988) | |
| 1987 | ||
| 1 | Ganesh Gopalakrishnan: Synthesizing Synchronous Digital VLSI Controllers Using Petri Nets. PNPM 1987: 94-103 | |