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.