Professor, School of Computing
Ph.D., State University of
New York at Stony Brook, 1986
Professor
Gopalakrishnan's primary research is in verification methods
for concurrent systems such as shared memory systems, microprocessor
busses, multithreaded software, and message passing networks. He also
maintains active interest in self-timed design. Today's concurrent
systems employ complex protocols that are expected to guarantee
properties such as in-order arrival of messages, deadlock freedom, and
liveness. In modern design approaches, these systems are subject to a
battery of conventional tests, and when all these pass, model-checking
methods are brought to bear to tracking down elusive bugs that may
cripple the system well after field deployment. The effectiveness of
conventional model-checking methods is limited by their inability to
handle large state spaces, deal with parameterized designs, or provide
guidelines for writing a comprehensive list of properties to
check. Our group's recent efforts have addressed these problems using
realistic driving problems such as generalized multi-level PCI I/O
busses, the Intel Itanium Shared Memory Model, and the Java Shared
Memory Model for Multithreading. Professor Gopalakrishnan was a
general co-Chair of the Internal Symposium on Formal Methods in
Computer-Aided Design (FMCAD) in November 1998, the International
Symposium on Advanced Research in Asynchronous Circuits and Systems
(Async) in November 1994. He organized the Workshop on Advances in
Verification (WAVe) as well as the workshop on Formal Specification
and Verification Methods for Shared Memory Systems, both in year 2000.
- Prosenjit Chatterjee and Ganesh Gopalakrishnan,
``Towards a Formal Model of Shared Memory Consistency
for Intel Itanium
,'' International Conference
on Computer Design, October 2001.
- Yue Yang, Ganesh Gopalakrishnan, and Gary Lindstrom,
``Analyzing the CRF Java Memory Model using Mur
,''
Workshop on Software Model Checking, July 2001 (Post CAV'01).
- Michael Jones and Ganesh Gopalakrishnan,
``Verifying Transaction Ordering Properties in Unbounded Multi-Bus
Networks through Algorithmic and Deductive Methods,''
Formal Methods in Computer-Aided Design, November 2000.
- Ravi Hosabettu, Ganesh Gopalakrishnan, and Mandayam Srivas,
``Verifying Microarchitectures that Support
Speculation and Exceptions,'' Computer Aided Verification,
July 2000.
- Hans Jacobson, Erik Brunvand, Ganesh Gopalakrishnan,
and Prabkahar Kudva, ``High Level Asynchronous
System Design Using the ACK Framework,''
Proc. Sixth
International Symposium on Advanced Research in
Asynchronous Circuits and Systems, April 2000.