The Nature of the PRL Project:
Background

Origins of the PRL Project

    The PRL research group was founded in 1979 by Joseph L. Bates and Robert L. Constable. It began as a project to build a logic-based program development system in which programs are constructed by interactive refinement. It combined ideas of Bates on program development by refinement with those of Constable on the design and automation of programming logics.

The Nuprl Systems

    Since 1984 the project has been concerned with a particular family of proof development systems (also called provers or verifiers or logical programming environments or problem solving environments). These systems realize our ideas on program development, programming logics, automated deduction, logic, foundations of computer science, formal methods, and programming languages and their environments. They have all been called Nuprl (pronounced "new pearl") which are instances (instance Greek "nu") of what we now call a Proof Refinement Logic (PRL).

    The identifiable versions have been Nuprl 1, Nuprl 3, Nuprl 4; and now we use and support Nuprl 4 while we are testing Nuprl 5.

Applications

    The technology that we have already deployed in Nuprl 4 is being applied to improve the reliability of real world software systems. In a joint project at Cornell with Ken Birman's distributed systems group, we have helped verify components of the Ensemble group communications system. Citation. We have developed a methodology that we call hardening of software that uses Nuprl to incrementally verify properties of software systems.

    At Bell Labs the HOL/Nuprl system created by Howe and Felty is being used in the verification of the SCI cache coherency protocol.

    We have experience in applying Nuprl to engineering problems from the work of Aagaard and Leeser in EE who used the system to verify circuits and CAD tools.