A Proof Environment for the Development of Group Communication Systems.
Christoph Kreitz, Mark Hayden, Jason Hickey.
In C. & H. Kirchner, eds., 15th International Conference on Automated Deduction (CADE-15), 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.

		Paper is available in postscript and pdf format		Slides of the conference presentation are available in compressed postscript and pdf format
Bibtex Entry					Back to overview of papers
	@InProceedings{inp:KreitzHaydenHickey98a, author = "Christoph Kreitz and Mark Hayden and Jason Hickey", title = "A Proof Environment for the Development of Group Communication Systems", booktitle = "15$^{th}$ International Conference on Automated Deduction", year = "1998", editor = "C. Kirchner and H. Kirchner", volume = "1421", series = "Lecture Notes in Artificial Intelligence", pages = "317--331", publisher = "Springer Verlag" }