Some Papers on ProofPower

Contributing Documentation Download Examples Getting Home Mailing List Papers Patches Specifications

This directory contains some papers about ProofPower.

The papers are supplied as PDF files where possible, otherwise as compressed PostScript format.

Methods and Tools for the Verification of Critical Properties: A paper by Roger Jones discussing (and illustrating using ProofPower) some methodological issues in the application of formal methods to critical systems.
On Formal Specification of a Proof Tool: A paper by Rob Arthan giving a simplified case study, in Z, illustrating the techniques which were used to specify ProofPower.
Development of Practical Verification Tools (PostScript): A paper by Dave King and Rob Arthan addressed at a general software engineering audience describing ProofPower and the Compliance Tool.

Roger Jones and Rob Arthan were the original architects of the ProofPower specification and verification systems. Dave King and Rob Arthan were the main designers of the ProofPower implementation of the Compliance Tool.

There are some more papers on formal methods by Rob Arthan in the papers section of the Lemma 1 web site.

Created by Rob Arthan [rda at lemma-one dot com]

Last updated: $Date: 2015/09/23 11:15:53 $