Skip to main content
SpringerLink
Log in
Book cover

International Conference on Automated Deduction

CADE 1998: Automated Deduction — CADE-15 pp 317–332Cite as

A proof environment for the development of group communication systems

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 1421))

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.

This is a preview of subscription content, log in via an institution.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. M. Archer & C. Heitmeyer. Mechanical verification of timed automata: A case study. Technical report, Naval Research Laboratory, Washington, DC, 1997.

    Google Scholar 

  2. W. Bibel, D. Korn, C. Kreitz, F. Kurucz, J. Otten, S. Schmitt, G. Stolpmann. A multi-level approach to program synthesis. In Seventh International Workshop on Logic Program Synthesis and Transformation, LNAI, Springer Verlag, 1998.

    Google Scholar 

  3. K. Birman. Building Secure and Reliable Network Applications. Manning Publishing Company and Prentice Hall, 1997.

    Google Scholar 

  4. K. Birman & R. van Renesse. Reliable Distributed Computing with the Isis Toolkit. IEEE Computer Society Press, 1994.

    Google Scholar 

  5. T. Chandra, V. Hadzilacos, S. Toueg, B. Charron-Bost. On the impossibility of group membership. 15th ACM Symposium on Principles of Distributed Computing, pp. 322–330, 1996.

    Google Scholar 

  6. R. Constable, et. al., Implementing Mathematics with the NuPRL proof development system. Prentice Hall, 1986.

    Google Scholar 

  7. D. de Rauglaudre. Camlp4 version 1.06. Institut National de Recherche en Informatique et en Automatique, 1997.

    Google Scholar 

  8. A. Fekete, N. Lynch, A. Shvartsman. Specifying and using a partitionable group communication service. In 16th ACM Symposium on Principles of Distributed Computing, 1997.

    Google Scholar 

  9. M. Gordon, R. Milner, C. Wadsworth. Edinburgh LCF: A mechanized Logic of Computation. LNCS 78, Springer Verlag, 1979.

    Google Scholar 

  10. O. Hafizogullari & C. Kreitz. Dead Code Elimination Through Type Inference. Technical Report TR 98-1698, Cornell University, 1998.

    Google Scholar 

  11. M. Hayden. Ensemble Reference Manual. Cornell University, 1996.

    Google Scholar 

  12. The Ensemble distributed communication system. System distribution and related information. http://www.cs.cornell.edu/Info/Projects/Ensemble

    Google Scholar 

  13. C. Kreitz. Formal mathematics for verifiably correct program synthesis. Journal of the IGPL, 4(1):75–94, 1996.

    MATH  MathSciNet  Google Scholar 

  14. C. Kreitz. Formal reasoning about communication systems I: Embedding ML into type theory. Technical Report TR97-1637, Cornell University, 1997.

    Google Scholar 

  15. C. Kreitz, J. Otten, S. Schmitt. Guiding Program Development Systems by a Connection Based Proof Strategy. In 5th International Workshop on Logic Program Synthesis and Transformation, LNCS 1048, pp. 137–151. Springer Verlag, 1996.

    Google Scholar 

  16. X. Leroy. The Objective Caml system release 1.06. Institut National de Recherche en Informatique et en Automatique, 1997.

    Google Scholar 

  17. N. Lynch. Distributed Algorithms. Morgan Kaufmann Publishers, 1996.

    Google Scholar 

  18. P. Lincoln & J. Rushby. A formally verified algorithm for interactive consistency under a hybrid fault model. In 23rd Fault-Tolerant Computing Symposium, pp. 402–411, 1993.

    Google Scholar 

  19. J. Rushby. Formal methods for dependable real-time systems. In International Symposium on Real-Time Embedded Processing for Space Applications, pp. 355–366, 1992.

    Google Scholar 

  20. J. Rushby. Systematic formal verification for fault-tolerant time-triggered algorithms. In Dependable Computing for Critical Applications: 6, pp. 191–210. IEEE Computer Society, 1997.

    Google Scholar 

  21. R. van Renesse, K. Birman, & S. Maffeis. Horus: A flexible group communication system. Communications of the ACM, 39(4):76–83, 1996.

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Cornell University, 14853-7501, Ithaca, NY, USA

    Christoph Kreitz, Mark Hayden & Jason Hickey

Authors
  1. Christoph Kreitz
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Mark Hayden
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Jason Hickey
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Claude Kirchner Hélène Kirchner

Rights and permissions

Reprints and permissions

Copyright information

© 1998 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Kreitz, C., Hayden, M., Hickey, J. (1998). A proof environment for the development of group communication systems. In: Kirchner, C., Kirchner, H. (eds) Automated Deduction — CADE-15. CADE 1998. Lecture Notes in Computer Science, vol 1421. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0054269

Download citation

  • DOI: https://doi.org/10.1007/BFb0054269

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-64675-4

  • Online ISBN: 978-3-540-69110-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation