Vita for GANESH GOPALAKRISHNAN -- 2/28/99 (items since 1/1/98 in boldface)
Department of Computer Science, University of Utah, Salt Lake City, UT 84112-9205
(801) 581-3568 (Fax 5843) -- ganesh@cs.utah.edu

EDUCATION

Ph.D. in Computer Science, State University of New York at Stony Brook, NY, Dec. 1986. Dissertation title: ``From Algebraic Specifications to Correct VLSI Systems''. Advisors: Profs.~D. R. Smith and M. K. Srivas.
M.Tech. in Electrical Engineering, Indian Institute of Technology, Kanpur, India, Aug. 1980.
B.Sc. in Electrical Engineering, Regional Engineering College, Calicut, India, Jan. 1978.

EMPLOYMENT

7/93 to present: Associate Professor, Computer Science, University of Utah, Salt Lake City,~UT.
9/95 to 5/96: On sabbatical leave at the Department of Computer Science, Stanford University, Stanford, CA.
9/86 to 6/93: Assistant Professor, Computer Science, University of Utah, Salt Lake City,~UT.
8/88 to 7/89: Visiting Assistant Professor of Computer Science, University of Calgary, Calgary, Alberta, Canada.
8/80 to 7/81: Research Associate, `Manpower Training in Microcomputers', Department of Computer Science, Indian Institute of Technology, Kanpur, India.

AREAS OF RESEARCH INTEREST

Formal verification of hardware systems (pipelined processors, shared memory systems, I/O systems), concurrent/reactive systems (concurrent/message-driven protocols), and circuits (register-transfer self-timed and synchronous circuits).
Design and automated synthesis of asynchronous (self-timed) circuits and systems, including new programmable asynchronous control structures.

ACCEPTED/PUBLISHED JOURNAL ARTICLES

1.: Hans M. Jacobson and Ganesh Gopalakrishnan, ``Application-Specific Programmable Control for Hihg-Performance Asynchronous Circuits'', Invited Paper, Proceedings of IEEE, Vol. 87, No. 2, Feb 1999, pp. 319--331. Appears in a special issue on the state of the art of asynchronous circuits and systems.
2.: Ratan Nalumasu and Ganesh Gopalakrishnan, ``Deriving Efficient Cache Coherence Protocols Through Refinement'', Formal Methods in System Design (Kluwer). (Submitted in 1998; to appear in a Special Issue in 1999.) A special issue based on the FMPPTA'98 workshop, Guest Editor: Dominique Mery.
3.: Jae-tack Yoo, Ganesh Gopalakrishnan, and Kent Smith, ``Timing Constraints for High Speed Counterflow-Clocked Pipelining'', IEEE Transactions on VLSI. (Submitted in 1995. To appear in 1999).
4.: Prabhakar Kudva, Ganesh Gopalakrishnan, and Erik Brunvand, ``Peephole Optimization of Asynchronous Macromodule Networks'', IEEE Transactions on VLSI. (Submitted in 1995. To appear in 1999).
5.: Jae-tack Yoo, Kent Smith, and Ganesh Gopalakrishnan, ``A Fast Parallel Squarer Based on Divide-and-Conquer'', IEEE Journal of Solid-state Circuits, Vol. 32, No. 6, pp. 909-912, June 1997.
6.: Venkatesh Akella and Ganesh Gopalakrishnan, ``CFSIM: A Concurrent Compiled Code Functional Simulator for hopCP'', International Journal of Computer Simulation, Vol. 4, No. 4, 1994, pp. 375-394. Special Issue on Computer Simulation of Application Specific Signal Processing Systems.
7.: Ganesh Gopalakrishnan, ``Micropipeline Wavefront Arbiters using Lockable C-elements'', IEEE Design Test of Computers, Winter 1994, Vol.11, No.4, pp.55-64. A special issue series on self-timed design.
8.: Venkatesh Akella and Ganesh Gopalakrishnan, ``Specification and Validation Control Intensive ICs in hopCP'', IEEE Transactions on Software Engineering, Vol.20, No.6, June 1994, pages 405-423.
9.: Prabhat Jain and Ganesh Gopalakrishnan, ``Efficient Symbolic Simulation Based Verification Using the Parametric Form of Boolean Expressions'', IEEE Transactions on Computer Aided Design, Vol.13, No.8, August 1994, pages 1005-1015.
10.: Ganesh Gopalakrishnan, Erik Brunvand, Nick Michell, and Steven M. Nowick, ``A Correctness Criterion for Asynchronous Circuit Validation and Optimization''. IEEE Transactions on Computer Aided Design, Vol.13, No.11, November 1994, pp. 1309-1318.
11.: Ganesh Gopalakrishnan and Venkatesh Akella, ``High Level Optimizations in Compiling Process Descriptions to Asynchronous Circuits'', Journal of VLSI Signal Processing (Kluwer), 7, 33-45 (1994). Special issue on Self-Timed Systems.
12.: Ganesh Gopalakrishnan and Richard Fujimoto, ``Design and Verification of the Rollback Chip using HOP: An Illustration of Formal Methods Applied to Hardware Design'', ACM Transactions on Computer Systems (TOCS), Vol.11, No.2, May 1993, pp. 109-145.
13.: Ganesh Gopalakrishnan and Venkatesh Akella, ``VLSI Asynchronous Systems: Specification and Synthesis'', Microprocessors Microsystems, Vol.16, No.10, October 1992, pp. 517-527.
14.: Richard M. Fujimoto, Jya-jang Tsai, and Ganesh Gopalakrishnan, ``Design and Evaluation of the Rollback Chip: Special Purpose Hardware for Time Warp'', IEEE Trans. on Computer, Vol.41, No.1, 1992, 68-82.
15.: Ganesh C. Gopalakrishnan, Richard Fujimoto, Venkatesh Akella, and Narayana Mani, ``HOP: A Process Model for Synchronous Hardware. Semantics, and Experiments in Process Composition.'', Integration: The VLSI Journal (North-Holland), 8 (1989), 209-247.
16.: Ganesh C. Gopalakrishnan and Mandayam K.~Srivas, ``Implementing Functional Programs Using Mutable Abstract Data Types'', Information Processing Letters, Vol.26, No.6, Jan 1988.

JOURNAL ARTICLES BEING REVISED

1.: Ratan Nalumasu and Ganesh Gopalakrishnan, ``A Partial Order Reduction Algorithm without the Proviso'', Formal Methods in System Design (Kluwer). (Submitted in 1998. Being revised.)
2.: Abdel Mokkedem, Ravi Hosabettu, and Ganesh Gopalakrishnan, ``Formalization and Proof of a Solution to the PCI 2.1 Bus Transaction Ordering Problem''. (Invited to a special issue of Formal Methods in System Design (Kluwer) being co guest-edited by me, based on FMCAD'98. Expected to appear in 1999.)

REFEREED PAPERS IN WORKSHOPS AND CONFERENCES

1.: (Accepted) Ravi Hosabettu, Mandayam Srivas, and Ganesh Gopalakrishnan, ``Proof of Correctness of a Processor with Reorder Buffer using the Completion Functions Approach'', Computer Aided Verification, 11th International Conference, CAV'99, July 1999, Trento, Italy.
2.: Ratan Nalumasu and Ganesh Gopalakrishnan, ``PV: an Explicit Enumeration Model-checker '', Formal Methods in Computer Aided Design, Second International Conference, FMCAD'98, Palo Alto, CA, USA, Nov 1998, Proceedings. Ganesh Gopalakrishnan and Phillip Windley (editors). Springer-Verlag LNCS 1522. pp. 523-528.
3.: Abdel Mokkedem, Ravi Hosabettu, and Ganesh Gopalakrishnan, ``Formalization and Proof of a Solution to the PCI 2.1 Bus Transaction Ordering Problem'', Formal Methods in Computer Aided Design, Second International Conference, FMCAD'98, Palo Alto, CA, USA, Nov 1998, Proceedings. Ganesh Gopalakrishnan and Phillip Windley (editors). Springer-Verlag LNCS 1522. pp. 237-254.
4.: Ratan Nalumasu, Rajnish Ghughal, Abdel Mokkedem, and Ganesh Gopalakrishnan, ``The `Test Model-checking' Approach to the Verification of Formal Memory Models of Multiprocessors'', Computer Aided Verification, 10th International Conference, CAV'98, Vancouver, B.C., Canada, June/July 1998, Proceedings. Alan J. Hu and Moshe Y. Vardi (editors). Springer-Verlag LNCS 1427. pp. 464-476.
5.: Ravi Hosabettu, Mandayam Srivas, and Ganesh Gopalakrishnan, ``Decomposing the Proof of Correctness of Pipelined Microprocessors'', Computer Aided Verification, 10th International Conference, CAV'98, Vancouver, B.C., Canada, June/July 1998, Proceedings. Alan J. Hu and Moshe Y. Vardi (editors). Springer-Verlag LNCS 1427. pp. 122-134.
6.: Rajnish Ghughal, Abdel Mokkedem, Ratan Nalumasu, and Ganesh Gopalakrishnan, ``Verification of the Runway-PA8000 memory model using Test Model-checking'', Symposium on Parallel Algorithms and Architectures (SPAA), 1998.
7.: Ratan Nalumasu and Ganesh Gopalakrishnan, ``Deriving Efficient Cache Coherence Protocols Through Refinement'', Formal Methods for Parallel Programming: Theory and Applications (FMPPTA'98), April 1998.
8.: Ganesh Gopalakrishnan, Rajnish Ghughal, Ravi Hosabettu, Abdel Mokkedem, and Ratan Nalumasu, ``Formal Modeling and Validation Applied to a Commercial Coherent Bus: A Case Study'', Proceedings of CHARME (Correct Hardware design Methods), Montreal, October, 1997, pp. 48-64.
9.: Hans Jacobson and Ganesh Gopalakrishnan, ``Asynchronous Microengines for Efficient High-level Control'', Advanced Research on VLSI (ARVLSI'97), Michigan, September 1997, pp. 201-218.
10.: Ratan Nalumasu and Ganesh Gopalakrishnan, ``PV: A Model-checker for Verifying LTL-X Properties'', Lfm97: Fourth NASA LaRC Formal Methods Workshop, 10-12 September 1997, Hampton, Virginia.
11.: Ratan Nalumasu and Ganesh Gopalakrishnan, ``A New Partial Order Reduction Algorithm for Concurrent System Verification'', Proceedings of the 1997 Computer Hardware Description Languages, Toledo, Spain, April 1997, pp. 305-314.
12.: Prabhakar Kudva, Ganesh Gopalakrishnan, and Hans Jacobson, ``A Technique for Synthesizing Distributed Burst-mode Circuits'', ACM 33rd Design Automation Conference (DAC'96), Las Vegas, NV, June 3-8, 1996, pp. 67-70.
13.: Prabhakar Kudva, Hans Jacobson, Ganesh Gopalakrishnan, and Steven M. Nowick, ``Synthesis of Hazard-free Customized CMOS Complex-gate Networks under Multiple-input Changes'', ACM 33rd Design Automation Conference (DAC'96), Las Vegas, NV, June 3-8, 1996, pp. 77-82.
14.: Prabhakar Kudva and Ganesh Gopalakrishnan, ``Techniques for Synthesizing Efficient Burst-mode Circuits'', In TAU, workshop on Timing Issues in the Specification and Synthesis of Digital Systems, Seattle, WA, Nov 10-11, 1995.
15.: Prabhakar Kudva, Ganesh Gopalakrishnan, and Venkatesh Akella, ``An Asynchronous High Level Synthesis System Targeted at Interacting Burst-Mode Controllers'', Proceedings of the 1995 Computer Hardware Description Languages, Chiba, Japan, pp. 605-610, August, 1995.
16.: Ratan Nalumasu and Ganesh Gopalakrishnan, ``Explicit-enumeration based Verification made Memory-efficient'', Proceedings of the 1995 Computer Hardware Description Languages, Chiba, Japan, pp. 617-622. August, 1995.
17.: Jae-Tack Yoo, Ganesh Gopalakrishnan, Kent Smith, and John Mathews, ``Counterflow-Clocked Pipelining Illustrated on the Design of High Speed HDTV Subband Vector Quantizer Chips'', Advanced Research on VLSI (ARVLSI'95), Chapel Hill, March 1995.
18.: Prabhakar Kudva, Ganesh Gopalakrishnan, and Erik Brunvand, ``Performance Analysis and Optimization of Asynchronous Circuits'', Intl. Conference on Computer Design (ICCD), 1994, pp. 221-224.
19.: Ganesh Gopalakrishnan, Prabhakar Kudva, Erik Brunvand, and Venkatesh Akella, ``Peephole Optimization of Asynchronous Networks through Process Composition and Burst-mode Machine Generation'', Intl. Conference on Computer Design (ICCD), 1994, pp. 442-446.
20.: Ganesh Gopalakrishnan and Lüli Josephson, ``Towards Amalgamating the Synchronous and Asynchronous Design Styles'', TAU '93, Timing Aspects of VLSI, Malente, Germany.
21.: Ganesh Gopalakrishnan and Venkatesh Akella, ``A Transformational Approach to Asynchronous High-level Synthesis'', VLSI '93, Grenoble, France, September 1993.
22.: John Hurdle, Lüli Josephson, Erik Brunvand, and Ganesh Gopalakrishnan, ``Asynchronous Models for Large Scale Neurocomputing Applications'', ``NEURO NIMES '92: Fifth International Conference on Neural Networks their Applications'', November 2-6, 1992, Nimes, France.
23.: Venkatesh Akella and Ganesh Gopalakrishnan, ``SHILPA: A High-level Synthesis System for Self-Timed Circuits'', accepted for publication in the International Conference on Computer Aided Design (ICCAD'92), Santa Clara, Nov. 1992.
24.: Armin Liebchen and Ganesh Gopalakrishnan. ``Dynamic Reordering of High Latency Transactions in Time-Warp Simulation Using a Modified Micropipeline'', International Conference on Computer Design (ICCD) 1992, pages 336 - 340.
25.: Prabhat Jain and Ganesh Gopalakrishnan. ``Efficient Symbolic Simulation Based Verification Using the Parametric form of Boolean Expressions'', International Conference on Computer Design (ICCD) 1992, 598-602.
26.: Prabhat Jain, Prabhakar Kudva, and Ganesh Gopalakrishnan, ``Towards a Verification Technique for Large Synchronous Circuits'', The Fourth Computer-Aided Verification Workshop (CAV'92), Montreal, June 1992.
27.: Venkatesh Akella and Ganesh Gopalakrishnan. ``Flow Analysis Techniques for the Synthesis of Efficient Asynchronous Circuits''. In TAU '92: 1992 Workshop on Timing Issues in the Specification and Synthesis of Digital Systems, Princeton, NJ, March 18--20, 1992.
28.: Venkatesh Akella and Ganesh Gopalakrishnan, ``Hierarchical Action Refinement: A Methodology for Compiling Asynchronous Circuits from a Concurrent HDL'', Proceedings of the Tenth International Symposium on Computer Hardware Description Languages and their Applications, Marseille, France, April 1991.
29.: Ganesh Gopalakrishnan and Prabhat Jain and Venkatesh Akella and Luli Josephson and Wen-Yan Kuo, ``Combining Verification and Simulation'', Advanced Research in VLSI (ARVLSI'91), Proceedings of the 1991 University of California Santa Cruz Conference, The MIT Press, 1991, Carlo Sequin (Ed.).
30.: Ganesh Gopalakrishnan and Prabhat Jain, ``A Practical Approach to Synchronous Hardware Verification'', in VLSI Design '91: The Fourth CSI/IEEE International Symposium on VLSI Design, January 5-8, 1991, New Delhi, India.
31.: Venkatesh Akella and Ganesh Gopalakrishnan, ``High Level Test Generation via Process Composition'', Designing Correct Circuits, Oxford, 1990, Springer Verlag, 99-119, Proceedings of the DCC Workshop, Oxford, September, 1990. (Published in Springer's new series `Workshops in Computing'.)
32.: Ganesh C. Gopalakrishnan, Narayana Mani, and Venkatesh Akella, ``A Design Validation System for Synchronous Hardware based on a Process Model: A Case Study'', IMEC-IFIP Workshop on `Applied Formal Methods for Correct VLSI Design', Nov.~13--16, Leuven, Belgium, 1989.
33.: Ganesh C. Gopalakrishnan, Richard M. Fujimoto, Venkatesh Akella, N.S. Mani, and Kevin Smith, ``Specification Driven Design of Custom VLSI Architectures in HOP'', G.~Birtwistle and P.A.~Subrahmanyam (editors), Current Trends in Hardware Verification and Automated Theorem Proving, Chapter 3, pages 128--170, Springer-Verlag, 1989.
34.: Ganesh C. Gopalakrishnan, ``Specification and Verification of Pipelined Hardware in HOP'', Ninth International Symposium on Computer Hardware Description Languages (CHDL'89), Washington, D.C., June, 1989, pp.117--131.
35.: Ganesh C. Gopalakrishnan, Narayana Mani, and Venkatesh Akella, ``Parallel Composition of Lock-step Synchronous Processes for Hardware Validation: Divide-and-conquer Composition'', in Springer Verlag Lecture Notes in Computer Science, No.407 (Automatic Verification Methods for Finite-State Systems, International Workshop, Grenoble, France, June 1989), pages 374-382. J.Sifakis (Editor).
36.: Richard M. Fujimoto, Jya-Jang Tsai and Ganesh C. Gopalakrishnan, ``Design and Performance Evaluation of the Roll Back Chip'', 1988 IEEE/ACM Computer Architecture Conference (ISCA'88), Honolulu, Hawaii, June 1988.
37.: Richard M. Fujimoto, Jya-Jang Tsai and Ganesh C. Gopalakrishnan, ``The Roll Back Chip: Hardware Support for Distributed Simulation Using Time Warp'', the Society for Computer Simulation Multiconference, San Diego, CA, Feb 1988.
38.: Ganesh C. Gopalakrishnan, ``Synthesizing Synchronous Digital VLSI Controllers Using Petri Nets'', Internal Workshop on Petri Nets and Performance Models, Wisconsin, August 24-26 (1987).
39.: Ganesh C. Gopalakrishnan, M.K.~Srivas, and D.R.~Smith, ``From Algebraic Specifications to Correct VLSI Circuits'', in book From HDL Descriptions to Guaranteed Correct Circuit Designs, D. Borrione (Ed.), IFIP, North-Holland (1987) 197-225.
40.: Ganesh C. Gopalakrishnan, N.C.Lee, D.R.Smith and M.K.Srivas, ``Deriving Module Interconnectivity From Behavioral Specifications and Coupling a VLSI Layout Editor for Error-free Routing'', 1986 Fall Joint Computer Conference, Dallas, Nov. 1986.
41.: Ganesh C. Gopalakrishnan, D.R.Smith, and M.K.Srivas, ``An Algebraic Approach to the Specification and Realization of VLSI Designs'', 7th International Symposium on Computer Hardware Description Languages (CHDL'85), Tokyo, Japan, Aug. 1985, North-Holland (1985) 16-38.

TECHNICAL REPORTS

1.: UUCS-98-017, Ratan Nalumasu and Ganesh Gopalakrishnan, ``A Partial Order Reduction Algorithm without the Proviso.''
2.: UUCS-98-008, Ratan Nalumasu, Rajnish Ghughal, Abdel Mokkedem, and Ganesh Gopalakrishnan, ``The Test Model-checking Approach to the Verification of Formal Memory Models of Multiprocessors.''
3.: UUCS-98-002, Ravi Hosabettu, Mandayam Srivas, and Ganesh Gopalakrishnan, ``Decomposing the Proof of Correctness of Pipelined Microprocessors.''
4.: UUCS-97-009, Ratan Nalumasu and Ganesh Gopalakrishnan, ``Deriving Efficient Cache Coherence Protocols through Refinement.''
5.: UUCS-97-007, Ganesh Gopalakrishnan, ``Application Specific Asynchronous Microengines for Efficient High-level Control.''
6.: UUCS-96-006, Ratan Nalumasu and Ganesh Gopalakrishnan, ``Partial Order Reduction Without the Proviso.''
7.: UUCS-95-019, Jae-Tack Yoo, Ganesh Gopalakrishnan, and Kent Smith, ``Timing Constraints for High Speed Counterflow-Clocked Pipelining.''
8.: UUCS-95-011, Jae-Tack Yoo, Kent Smith, and Ganesh Gopalakrishnan, ``A Fast Parallel Squarer Based on Divide-and-Conquer.''
9.: UUCS-95-006, Ratan Nalumasu and Ganesh Gopalakrishnan, ``Explicit-enumeration based Verification made Memory-efficient.''
10.: UUCS-94-009, Ganesh Gopalakrishnan, Dilip Khandekar, Ravi Kuramkote, and Ratan Nalumasu, ``Case Studies in Symbolic Model Checking.''
11.: UUCS-93-020, Ganesh Gopalakrishnan, Prabhakar Kudva, and Erik Brunvand, ``Peephole Optimization of Asynchronous Networks through Process Composition and Burst-mode Machine Generation.''
12.: UUCS-93-017, Prabhakar Kudva, Ganesh Gopalakrishnan, Erik Brunvand, and Venkatesh Akella, ``A Transformational Approach to Asynchronous High-Level Synthesis.''
13.: UUCS-93-015, Ganesh Gopalakrishnan, ``Some Unusual Micropipeline Circuits.''
14.: UUCS-92-019a, Venkatesh Akella and Ganesh Gopalakrishnan, ``High Level Optimizations In Compiling Process Descriptions To Asynchronous Circuits.''
15.: UUCS-92-012, Prabhat Jain and Ganesh Gopalakrishnan, ``Towards A Verification Technique for Large Synchronous Circuits.''
16.: UUCS-92-009a, Ganesh Gopalakrishnan, ``HOP: A Formal Model for Synchronous Circuits using Communicating Fundamental Mode Symbolic Automata.''
17.: UUCS-92-008, Ganesh Gopalakrishnan, ``Asynchronous Circuit Verification Using Trace Theory and CCS.''
18.: UUCS-92-005, Armin Liebchen and Ganesh Gopalakrishnan, ``Dynamic Reordering of High Latency Transactions in Time-Warp Simulation Using a Modified Micropipeline''.
19.: UUCS-92-004, Ganesh Gopalakrishnan, Erik Brunvand, Nick Mitchell, and Steven M. Nowick, ``A Correctness Criterion for Asynchronous Circuit Validation and Optimization.''
20.: UUCS-92-001, Venkatesh Akella and Ganesh Gopalakrishnan, ``Specification and Validation of Control Intensive ICs in hopCP''.
21.: UUCS-91-023, Prabhat Jain and Ganesh Gopalakrishnan, ``Efficient Symbolic Simulation Based Verification Using the Parametric form of Boolean Expressions''.
22.: UUCS-91-018, Venkatesh Akella and Ganesh Gopalakrishnan, ``Flow Analysis Techniques for the Synthesis of Efficient.''
23.: UUCS-90-016, Prabhat Jain and Ganesh Gopalakrishnan, ``Some Recent Asynchronous Design Methodologies''.

PROFESSIONAL ACTIVITIES

Member, IFIP WG 10.5, 1993-present.
Co-editor (with Phillip Windley), Special Issue of Formal Methods in System Design (Kluwer), ``Formal Methods: Technologies and Trends''. Special Issue slated for 1999.
Program Committee Member, International Conference on Computer Design (ICCD), 1999.
Site Reviewer, 1999, NSF Science and Technology Center competition, SUNY, Stony Brook, NY.
External Ph.D. examiner, Dept of Computer Science (IRO), University of Montreal, Canada, 1999.
Program Committee Member, and Tutorials Chair, Async'99: Fifth International Conference on Advanced Research in Asynchronous Circuits and Systems, Barcelona, April 1999.
Program Committee Member, CHARME (IFIP WG 10.2/10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods), Germany, 1999.
General co-Chair (with Phillip Windley), Internal Symposium on Formal Methods in Computer-Aided Design (FMCAD), November 1998.
Member, NSF panel (CISE/CCR), Software Engineering and Languages program, Feb 4, 1998.
Member, Organizing Committee of the 21st Century Engineering Consortium Workshop on Formal Methods Education, Sponsored by Rome Labs, DARPA. Melbourne, Florida, March, 1998.
Member of panel and session chair, Async'98: Fourth International Conference on Advanced Research in Asynchronous Circuits and Systems, San Diego, CA, March 1998.
Session chair, session on ``Formal Characterizations of Systems'', International Symposium on Computer Hardware Description Languages (CHDL), 1997, Toledo, Spain, April 1997.
Program Committee Member, International Symposium on Computer Hardware Description Languages (CHDL), 1997, Spain.
Program Committee Member, CHARME (IFIP WG 10.2/10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods), Montreal, Canada, October 1997.
External Ph.D. examiner, Computer Science, University of Adelaide, 1997.
External Ph.D. examiner, Dept of Computer Science (IRO), University of Montreal, Canada, 1996.
Program Committee Member, International Symposium on Computer Hardware Description Languages (CHDL), 1995, Tokyo, Japan.
Session co-chair, session on ``Computer Representations for Verification'', International Symposium on Computer Hardware Description Languages (CHDL), 1995, Tokyo, Japan.
External Ph.D. examiner, Electrical and Computer Engineering, University of Calgary, Canada, July 1995.
External Ph.D. examiner, Computer Science, Monash University, Clayton, Australia, May 1995.
Founding Co-chair for the ``Symposium on Advanced Research on Asynchronous Circuits and Systems'', Salt Lake City, UT, November 3-5, 1994.
Co-guest editor (with Erik Brunvand) of a special issue ``Asynchronous Circuits: CAD Tools, and Significant Applications'', in Integration, The VLSI Journal, October 1993.
Co-organizer (with Erik Brunvand) a 1.5-day ``mini-track'' on self-timed systems as part of the 26th Hawaiian International Conference on Systems Sciences (HICSS), January, 1993.
Member of a panel discussion on ``Why do Asynchronous Systems Matter?'', during TAU '92: 1992 Workshop on Timing Issues in the Specification and Synthesis of Digital Systems, Princeton, NJ, March 18--20, 1992.
External Ph.D. examiner, Department of Computer Science, University of Glasgow, UK, Sep 13, 1991.

INVITED TALKS

1.

``Formal verification of Conformance to Memory Models'', invited talk given at the Dept. of Computer Science, University of Austin, October 1999.

2.

``1-day Tutorial on Formal Methods'', given at the Indian Institute of Technology, Bombay, India, and the Indian Institute of Science, Bangalore, India, June/July, 1998.

3.

``The Utah Verifier Project'', presented at Stanford University, Nov 17, 1997.

4.

``Formal Methods work in the Utah Verifier group'', talk at the Naval Research Labs, Washington D.C., Nov 3, 1997.

5.

``Applying Formal Methods to System Level Hardware Designs'', colloquium at the University of Montreal, April 8, 1997.

6.

``Applying Formal Methods to System Level Hardware Designs'', presented at Sun Microsystems Laboratories, Menlo Park, March 4, 1997.

7.

``The Avalanche Scalable Parallel Processor: An Overview of its Design and Formal Validation'', given at

(a): Hewlett-Packard Laboratories, Palo Alto, CA, July 9, 1996.
(b): Hewlett-Packard General Systems Laboratories, Roseville, CA, Feb 12, 1996.
(c): University of California, Davis, Feb 13, 1996.
(d): Stanford Research Institute, Feb 15, 1996.

8.

``Some Experiments with Explicit Enumeration'', Invited talk at the Workshop on Higher-Order Logic Theorem Proving and Its Applications, Aspen Grove, UT, USA. September, 1995.

9.

``Specification Driven Design of Hardware'', Computer Science Department, University of Calgary, November 29, 1991.

10.

``Design and Verification of the Roll Back Chip'', Computer Science Department, University of Glasgow, Glasgow, Scotland, U.K., September 12, 1991.

11.

``Combining Verification and Simulation'', Computer Science Department, University of Waterloo, Waterloo, Canada, July 5, 1991.

12.

``Combining Verification and Simulation'', Computer Science Department, Indian Institute of Science, Bangalore, India, December, 1990.

13.

``Combining Verification and Simulation'', Computer Science Department, University of Oregon, Eugene, OR, November, 1990.

14.

``A Process Model for Synchronous Hardware'', at the Computer Science Departments of:

(a): University of Indiana, Bloomington, April 5, 1990;
(b): University of Montreal, Montreal, Canada, April 3, 1990;
(c): SUNY Albany, April 2, 1990.

15.

``Formalization of an Operational Approach to Hardware Specification and Validation''. Invited talk given at the 1989 Banff Workshop on Type Theory and Higher Order Logic, Graham Birtwistle (organizer), Banff Centre, Canada, September 13--28.

16.

``Hardware Specification and Validation Using HOP'', Laboratory for Automation, Communication, and Information Systems Research, Department of Computer Science, University of Victoria, Vancouver, British Columbia, Canada, July 28, 1989.

17.

``Specification of Pipelined Hardware in HOP'', Computer Science Department, Simon Fraser University, Burnaby, British Columbia, April 1989.

18.

``HOP: A Language for Specification, Verification and Design Automation'', given at the Micro-electronics and Computer Corporation (MCC), Austin, Texas, January 1988.

19.

Ten job-interview related talks.

SOFTWARE PROJECTS

1.: ACK (``Asynchronous Circuit Kompiler''), a high-level synthesis tool for asynchronous circuits, by former PhD student Prabhakar Kudva. Rewritten by current PhD student Hans Jacobson.
2.: PV (``Protocol Verifier''), an explicit enumeration tool, by former PhD student Ratan Nalumasu. In routine use. Demoed at the Fourth NASA LaRC Formal Methods Workshop, and FMCAD'98.
3.: SHILPA (``System for HIgh Level synthesis of Processes to Asynchronous circuits''), by former PhD student Venkatesh Akella. Demoed during DAC'92.
4.: HOP (``Hardware modeled as Objects and Processes''), by myself and former Master's student Mani. Demoed at the workshop ``Automatic Verification Methods for Finite-State Systems'', Grenoble, France, Jun.~1989, and the IMEC-IFIP Workshop on ``Applied Formal Methods for Correct VLSI Design'', Nov.~13--16, Leuven, Belgium, 1989.
5.: Beta testing for Tanenbaum's Minix, 1987.
6.: SBL (``Structure and Behavior Language''), an algebraic modeling language for VLSI, and its high-level simulator. Developed as part of my PhD. Stony Brook, 1986.
7.: Run-time support routines for a Prolog Compiler in the MC-68000 assembly language. Stony Brook, 1984.
8.: Brutus, an interactive Graphics Editor for VLSI Design, Stony Brook, 1983.
9.: VLSI mask manipulation algorithms in Bell Labs, Murray Hill, NJ, 1983. Software used in Bell Lab's GRED graphical VLSI mask editor.
10.: Adaptation of Tim Saxe's CLL (Chip Layout Language) from NMOS to CMOS. Stony Brook, 1983.

GRANTS/AWARDS ...

PhD COMMITTEES CHAIRED

1.: Hans Jacobson
2.: Ravi Hosabettu
3.: Mike Jones
4.: Annette Bunker
5.: Ratan Nalumasu --- W99 --- Staff Scientist, HP, Cupertino
6.: Prabhakar Kudva --- W96 --- Researcher, IBM Yorktown Heights
7.: Venkatesh Akella --- F92 --- Associate Professor, Dept. ECE, UC Davis

MEMBER OF OTHER PhD COMMITTEES

1.: Hao Zheng
2.: Wendy Belluomini
3.: Ajay Khoche, 96
4.: Jae-tack Yoo, 95
5.: Surya Mantha, 93
6.: Wen Yan Kuo, 90
7.: Stanley Shebs, 89

MS COMMITTEES CHAIRED

1.: Prabhakar Kudva --- F92
2.: Prabhat Jain --- S92
3.: Narayana Mani --- S89

MEMBER OF OTHER MS COMMITTEES

1.: Marshall Soares, 97
2.: Robert Thacker, 97
3.: V. Chandramouli, 94
4.: Anilkumar Sabbavarappu, 92
5.: Cary Boyd, 90
6.: Jeff Smith, 90
7.: Kevin Smith, 89
8.: H.K. Yang, 88
9.: Hwa-chung Feng, 87

NEW COURSES INTRODUCED

1.: CPSC 6933, Hardware Emulation: W99-semester
2.: CS 611, Formal Methods for System Design: F96, 97
3.: CS 573, Logic for Computer Science: S93.
4.: CS 611, Program Verification: F86, F87, F89, F90, F91, F93, F94 and W92
5.: CS 570, High Level Synthesis of VLSI: F91.
6.: CS 577, Asynchronous Systems: W90.

OTHER COURSES TAUGHT

1.: CPSC 5100, Foundations of Computer Science: F98-semester
2.: CS 511, Programming Languages: S98
3.: CS 505, Introduction to Theoretical Computer Science: W98
4.: EE/CS 552, Microprocessor Design Laboratory: S97
5.: EE/CS 551, Microprocessor Laboratory: W97
6.: CS 511, Programming Linguistics: S90, S91, S95
7.: EE/CS 563, Microprocessor Laboratory: W95
8.: EE/CS 564, Microprocessor Design Laboratory: S95
9.: CS 561, Advanced Computer Organization: W93
10.: CS 506, Operating Systems: W87, F92.
11.: CS 507, Compilers: S92
12.: CS 541, Modeling Integrated Circuits: W91
13.: CPSC 463 (Calgary) VLSI Design: W89
14.: CPSC 433 (Calgary) Inference and Automation of Reasoning: F88
15.: CS 451, Software Engineering Laboratory series: F87, W88, S88

COLLEGE COMMITTEES

1990-92: College Council representative for CS.

DEPARTMENT COMMITTEES

1.: 1998-99: Director of Graduate Admissions, Comprehensive Exams.
2.: 1997-98: Departmental RPT Chair, Comprehensive Exams.
3.: 1996-97: Computer Engineering, Computer Policies.
4.: 1994-95: Undergraduate, Computer Engineering.
5.: 1993-94: Undergraduate, Computer Engineering.
6.: 1992-93: Colloquium chair.
7.: 1990-92: Graduate Committee.
8.: 1989-90: Faculty Recruiting, Curriculum.
9.: 1987-88: Grad. Admissions.
10.: 1986-94: Library representative for the Department.

REVIEWING

: Formal Methods in System Design (1999).
: IEEE Transactions on Computer Aided Design (1993, 94, 95, 96, two in 1997, 1998)
: NSF (average one a year for all the years)
: Program committee work for Charme'97 (several papers)
: Computer Hardware Description Languages Conference (1988, 1995, 1996)
: Advanced Research in Asynchronous Circuits and Systems (1995, 1998)
: Journal of Formal Methods (1993, 2 in 1995, 2 in 1996)
: Operating Systems Design and Implementation (OSDI) Conference (1995)
: Swedish Research Council for Engineering Sciences (1995)
: NSERC, Canada (1995)
: Design Test of Computers (1993)
: IEEE Transactions on Computer (1995)
: IEEE Transactions on VLSI Systems (1993, 1997)
: IEEE Computer (1986, 87, 88, 89)
: IEEE Software (1985, 87, 88)
: Integration, the VLSI Journal (1992)
: Journal of VLSI and Signal Processing (1992)
: International Journal of Parallel Programming (1987, 89)
: Journal of Computers and Electrical Engineering (1992)
: Functional Programming and Computer Architecture Conference (1991)
: Fault Tolerant Computing Systems (FTCS) Conference (1991)
: IFIP Workshop ``Applied Formal Methods for Correct VLSI Design'' (1989)
: CONCUR (1992)
: CAV (1992)
: NSERC (1993, 1996)
: Swedish Research Council for Engineering Sciences (1993)