A Proof Environment for the Development of Group Communication Systems

unofficial copies [PDF], [PS]


by Christoph Kreitz, Mark Hayden, and Jason Hickey

Proceedings of 15th International Conference on Automated Deduction (CADE-15), C. and H. Kirchner (eds.), LNAI 1421, pp. 317-331, Springer-Verlag, 1998.

Abstract

We present a logical programming environment for the development of reliable and efficient group communication systems. Our approach makes methods of automated deduction applicable to the implementation of real-world systems by integrating the Ensemble group communication toolkit with the NuPRL proof development system.

We will present tools for importing Ensemble's code into the logical language of NuPRL and exporting it back into the programming environment. We will discuss techniques for reasoning about critical properties of Ensemble as well as verified strategies for reconfiguring the Ensemble system in order to improve its performance in particular applications.


Slides of the conference presentation are available in compressed PS and PDF format.