Designing Reliable, High-Performance Networks in the Nuprl Programming Environment

Christoph Kreitz

Our goal is to demonstrate that the NUPRLPE is capable of supporting the formal design and implementation of large-scale, high-performance network systems. We have already used the NUPRLPE in the verification of protocols for the ENSEMBLE group communication toolkit (Kreitz, Hayden, and Hickey 1998; Hickey, Lynch, and van Renesse 1999), in verifiably correct optimizations of ENSEMBLE protocol stacks (Kreitz 1999; Liu et al. 1999), and in the formed design and implementation of new adaptive network protocols (Liu et al. 2001; Bickford et al. 2001a; 2001b). Currently we are working on providing formal support for the development of large distributed embedded systoms.


This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.