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.