BCS is a registered charity: No 292786
3rd Irish Workshop on Formal Methods
Galway, Ireland. 1st - 2nd July 1999
J.C. Bicarregui & B.M. Matthews
In this paper we describe investigations into the use of automatic theorem proving technology in the refutation of proof obligations.
Specifically, we discuss the use of resolution based theorem proving and model checking to find false obligations and counterexamples.
These techniques can be used as basis of an automatic method for finding faults in design during the formal development of software.
This approach is complementary to verification by proof as such proofs can only be completed when all faults have been corrected. We give a simple example using the B formal development method to demonstrate its potential.