The ProofPower Web Pages
[ProofPower Logo]


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:

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:

E-mail enquiries may be addressed to: [rda at lemma-one dot com]

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

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

Copyright © Lemma 1 Ltd.
Created by  Rob Arthan [rda at lemma-one dot com]
Last updated: $Date: 2017/03/11 16:15:43 $
[Lemma 1 Logo]