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

Logic-Based Program Synthesis: State of the Art and Future Trends

Volume

Papers from the 2002 AAAI Spring Symposium

Contents

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.