The ProofPower Web Pages (original) (raw)

The ProofPower Web Pages

| | | | ----------------------------------------------------------------- | |

Contributing Documentation Download Examples Getting Home Mailing List Papers Patches Specifications

ProofPower is a suite of tools supporting specification and proof in Higher Order Logic (HOL) and in the Z notation. The suite comprises the following packages:

• PPDev - The ProofPower developer kit, mainly comprising SLRP, a parser generator for Standard ML.
• PPTex - The ProofPower interface to TeX and LaTeX.
• PPXpp - The X Windows/Motif front-end for ProofPower.
• PPHol - The HOL specification and proof development system.
• PPZed - The Z specification and proof development system.
• PPDaz - The Compliance Tool for specifying and verifying Ada programs.

All the ProofPower packages except PPDaz are free, open-source, software made available under the terms of the GNU General Public License.

ProofPower has been under ongoing development since 1989. It was originally designed and implemented by International Computers Ltd. to support proofs of specification-to-model correspondence for high-assurance secure systems. It has since played an important role in approaches to specifying and verifying safety-critical systems in work by the Defence and Evaluation Research Agency (DERA), now QinetiQ. The research themes involving ProofPower that were initiated at DERA and QinetiQ are now being actively exploited by D-RisQ Limited.. Since 1997, on-going developments to the product have been undertaken by Lemma 1 Ltd. In Spring 2000, International Computers Ltd. transferred its rights in ProofPower to Lemma 1 Ltd who now maintain this web site and support and distribute the software.

The information currently available on this site comprises:

• The ProofPower FAQ.
• A selection of specification and proof scripts.
• Instructions for getting the ProofPower software, its documentation and upgrades and fixes.
• Some information about contributing to ProofPower.
• Some papers written by members of the ProofPower development team.
• Some examples of ProofPower in action to supplement the examples supplied with the system.

E-mail enquiries may be addressed to:

There is a mailing listfor general discussion of all kinds about ProofPower.

`ProofPower' is a registered trade mark of Lemma 1 Ltd.