| 2009 |
|---|
| 93 | EE | Anh Vo,
Sarvani S. Vakkalanka,
Michael Delisi,
Ganesh Gopalakrishnan,
Robert M. Kirby,
Rajeev Thakur:
Formal verification of practical MPI programs.
PPOPP 2009: 261-270 |
| 2008 |
|---|
| 92 | EE | Chao Wang,
Yu Yang,
Aarti Gupta,
Ganesh Gopalakrishnan:
Dynamic Model Checking with Property Driven Pruning to Detect Race Conditions.
ATVA 2008: 126-140 |
| 91 | EE | 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 | EE | Ganesh Gopalakrishnan,
Robert M. Kirby:
Runtime verification methods for MPI.
IPDPS 2008: 1-5 |
| 89 | EE | Sarvani S. Vakkalanka,
Michael Delisi,
Ganesh Gopalakrishnan,
Robert M. Kirby:
Scheduling considerations for building dynamic verification tools for MPI.
PADTAD 2008: 3 |
| 88 | EE | Guodong Li,
Michael Delisi,
Ganesh Gopalakrishnan,
Robert M. Kirby:
Formal specification of the MPI-2.0 standard in TLA+.
PPOPP 2008: 283-284 |
| 87 | EE | Sarvani S. Vakkalanka,
Subodh Sharma,
Ganesh Gopalakrishnan,
Robert M. Kirby:
ISP: a tool for model checking MPI programs.
PPOPP 2008: 285-286 |
| 86 | EE | 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 | EE | 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 | EE | Yu Yang,
Xiaofang Chen,
Ganesh Gopalakrishnan,
Robert M. Kirby:
Efficient Stateful Dynamic Partial Order Reduction.
SPIN 2008: 288-305 |
| 83 | EE | Ganesh Gopalakrishnan:
Review computation engineering: applied automata theory and logic.
SIGACT News 39(3): 30-32 (2008) |
| 2007 |
|---|
| 82 | EE | Xiaofang Chen,
Steven M. German,
Ganesh Gopalakrishnan:
Transaction Based Modeling and Verification of Hardware Protocols.
FMCAD 2007: 53-61 |
| 81 | EE | Robert Palmer,
Michael Delisi,
Ganesh Gopalakrishnan,
Robert M. Kirby:
An Approach to Formalization and Analysis of Message Passing Libraries.
FMICS 2007: 164-181 |
| 80 | EE | Ganesh Gopalakrishnan,
Robert M. Kirby:
Formal Analysis for Debugging and Performance Optimization of MPI.
IPDPS 2007: 1-6 |
| 79 | EE | Robert Palmer,
Ganesh Gopalakrishnan,
Robert M. Kirby:
Semantics driven dynamic partial-order reduction of MPI-based parallel programs.
PADTAD 2007: 43-53 |
| 78 | EE | 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 | EE | Yu Yang,
Xiaofang Chen,
Ganesh Gopalakrishnan,
Robert M. Kirby:
Distributed Dynamic Partial Order Reduction Based Verification of Threaded Software.
SPIN 2007: 58-75 |
| 76 | EE | Ganesh Gopalakrishnan,
John O'Leary:
Preface.
Electr. Notes Theor. Comput. Sci. 174(9): 1-4 (2007) |
| 75 | EE | Ganesh Gopalakrishnan:
Preface.
Electr. Notes Theor. Comput. Sci. 193: 1-2 (2007) |
| 74 | EE | Ganesh Gopalakrishnan,
Robert M. Kirby:
Formal Methods for MPI Programs.
Electr. Notes Theor. Comput. Sci. 193: 19-27 (2007) |
| 2006 |
|---|
| 73 | EE | 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 | EE | Ganesh Gopalakrishnan,
Robert M. Kirby:
Toward reliable and efficient message passing software through formal analysis.
IPDPS 2006 |
| 71 | EE | 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 | EE | 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 | EE | Ritwik Bhattacharya,
Steven M. German,
Ganesh Gopalakrishnan:
Exploiting Symmetry and Transactions for Partial Order Reduction of Rule Based Specifications.
SPIN 2006: 252-270 |
| 68 | EE | 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 | EE | Sudhindra Pandav,
Konrad Slind,
Ganesh Gopalakrishnan:
Counterexample Guided Invariant Discovery for Parameterized Cache Coherence Verification.
CHARME 2005: 317-331 |
| 66 | EE | Ritwik Bhattacharya,
Steven M. German,
Ganesh Gopalakrishnan:
Symbolic Partial Order Reduction for Rule Based Transition Systems.
CHARME 2005: 332-335 |
| 65 | EE | Ali Sezgin,
Ganesh Gopalakrishnan:
On the decidability of shared memory consistency verification.
MEMOCODE 2005: 199-208 |
| 64 | EE | 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 | EE | Ali Sezgin,
Ganesh Gopalakrishnan:
On the definition of sequential consistency.
Inf. Process. Lett. 96(6): 193-196 (2005) |
| 62 | EE | 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 | EE | Ganesh Gopalakrishnan,
Yue Yang,
Hemanthkumar Sivaraj:
QB or Not QB: An Efficient Execution Verification Tool for Memory Orderings.
CAV 2004: 401-413 |
| 59 | EE | Yue Yang,
Ganesh Gopalakrishnan,
Gary Lindstrom:
Memory-Model-Sensitive Data Race Analysis.
ICFEM 2004: 30-45 |
| 58 | EE | Yue Yang,
Ganesh Gopalakrishnan,
Gary Lindstrom,
Konrad Slind:
Nemos: A Framework for Axiomatic and Executable Specifications of Memory Consistency Models.
IPDPS 2004 |
| 57 | EE | 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 | EE | 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 | EE | Hemanthkumar Sivaraj,
Ganesh Gopalakrishnan:
Random Walk Based Heuristic Algorithms for Distributed Memory Model Checking.
Electr. Notes Theor. Comput. Sci. 89(1): (2003) |
| 54 | EE | 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 | EE | 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 | EE | 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 | EE | Prosenjit Chatterjee,
Hemanthkumar Sivaraj,
Ganesh Gopalakrishnan:
Shared Memory Consistency Protocol Verification Against Weak Memory Models: Refinement via Model-Checking.
CAV 2002: 123-136 |
| 50 | EE | Prosenjit Chatterjee,
Ganesh Gopalakrishnan:
A Specification and Verification Framework for Developing Weak Shared Memory Consistency Protocols.
FMCAD 2002: 292-309 |
| 49 | EE | Robert Palmer,
Ganesh Gopalakrishnan:
A Distributed Partial Order Reduction Algorithm.
FORTE 2002: 370 |
| 48 | EE | Yue Yang,
Ganesh Gopalakrishnan,
Gary Lindstrom:
Specifying Java thread semantics using a uniform memory model.
Java Grande 2002: 192-201 |
| 47 | EE | 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 | EE | 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 | EE | 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 | EE | 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 | EE | 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 | EE | 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 | EE | Ganesh Gopalakrishnan,
Prabhakar Kudva,
Erik Brunvand:
Peephole optimization of asynchronous macromodule networks.
IEEE Trans. VLSI Syst. 7(1): 30-37 (1999) |
| 33 | EE | 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 | EE | 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 | EE | 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 | EE | 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 | EE | 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 | EE | Prabhakar Kudva,
Ganesh Gopalakrishnan,
Hans M. Jacobson:
A Technique for Synthesizing Distributed Burst-mode Circuits.
DAC 1996: 67-70 |
| 22 | EE | 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 | EE | 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 | EE | Ganesh Gopalakrishnan:
Developing Micropipeline Wavefront Arbiters.
IEEE Design & Test of Computers 11(4): 55-64 (1994) |
| 17 | EE | Venkatesh Akella,
Ganesh Gopalakrishnan:
Specification and Validation of Control-Intensive IC's in hopCP.
IEEE Trans. Software Eng. 20(6): 405-423 (1994) |
| 16 | EE | 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 | EE | 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 | EE | 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 | EE | 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 | EE | 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 |
