David A. Karr
Project
I am collaborating with Rick Schantz, Dave Bakken, John Zinky, and others on the Adaptive Quality of Service for Availability (AQuA) project in the Distributed Systems department of the BBN Technologies division of GTE Internetworking.
Interests
I am interested in general in software systems in which processing is distributed over a wide-area network. The problems in this area include not only correct execution of the software's functions (where we must be concerned about failure of hosts and inconsistency among processes), but also issues of availability, response time, and efficient use of resources in which the wide-area network environment poses special challenges. An advantage of the QuO architecture in this environment is that it can detect and adapt to changes in system conditions that may result either from transient network events or from longer-term changes in system configuration.
My Ph.D. work concentrated on the formal specification and verification of the properties of Horus protocol layers. Using the Temporal Logic of Actions, one can specify Horus protocol stacks, or their individual layers, in terms of the communication properties they require from the network or other layers underneath them, and the properties they then support for the layers above. Moreover, it is feasible to automatically verify the properties of protocol stacks, given suitable specifications of the layers in the stack. This work was performed as part of the Securing and Hardening Horus project at Cornell University. I have developed a Java applet that gives a rough demonstration of the method of verifying the properties of Horus protocol stacks.
Publications
Robbert van Renesse, Ken Birman, Mark Hayden, Alexey Vaysburd, and David Karr. Building Adaptive Systems Using Ensemble. Technical Report number TR97-1638. Department of Computer Science, Cornell University, Ithaca, NY, July 1997.
David A. Karr. Specification, Composition, and Automated Verification of Layered Communication Protocols. Doctoral dissertation. Technical Report number TR97-1623. Department of Computer Science, Cornell University, Ithaca, NY, March 1997.
Robbert van Renesse, Kenneth P. Birman, Roy Friedman, Mark Hayden, and David A. Karr. A framework for protocol composition in Horus. In Proceedings of the 14th Annual ACM Symposium on Principles of Distributed Computing, pp. 80-89. ACM, August 1995.
Professional Affiliations
I am employed by BBN Technologies, a division of GTE Networking, in Cambridge, Massachusetts.
I am a member of IEEE and ACM.
Education
Cornell University. Ph.D. in Computer Science.
Harvard University. B.A. in Mathematics.
