A Proof Environment for the Development of Group Communication Systems
by Christoph Kreitz, Mark Hayden, Jason Hickey
Proceedings of 15th International Conference on Automated Deduction (CADE-15), C. and H. Kirchner (eds.), LNAI 1421, pp. 317-331, Springer-Verlag
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.
bibTex ref: KHH98