A Proof Environment for the Development of Group Communication Systems

Abstract. We present a theorem proving 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 linking the Ensemble group communication toolkit to the NuPRL proof development system. We present tools for importing Ensemble's code into NuPRL and exporting it back into the programming environment. We 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 concrete applications.

• Type: Conference
• Year: 1998
• Where: CADE
• Authors: Christoph Kreitz, Mark Hayden, Jason Hickey
• Keywords: CADE 1998, Ensemble Group Communication, Logical Reasoning, Nuprl Proof Development, Theorem Proving Environment