ePubs

The open archive for STFC research publications

Full Record Details

Persistent URL http://purl.org/net/epubs/work/38103
Record Status Checked
Record Id 38103
Title Proof and Refutation in Formal Software Development
Contributors
Abstract 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.
Organisation CCLRC , ESC
Keywords B Method , Formal Methods , Model Checking , Proof , Software Engineering
Funding Information
Related Research Object(s):
Licence Information:
Language English (EN)
Type Details URI(s) Local file(s) Year
Paper In Conference Proceedings In 3rd Irish Workshop on Formal Methods (IWFM'99), Galway, Ireland, 1-2 Jul 1999, (1999). refutation.ps
proofrefutationinsoftware.pdf		 1999