[Prev][Next][Index]

FWD: mechanical program/system verification request

[I am pointing him at the Larch Home Page...]

------- Forwarded Message

From: aaron@mmml.demon.co.uk (Aaron Turner)
Date: Sun, 20 Nov 1994 16:58:20 +0000
Subject: mechanical program/system verification
Newsgroups: comp.specification
Reply-To: aaron@mmml.demon.co.uk

I am trying to put together a definitive review of the current state of
program / system verification in both theory and practice. By verification I
mean the use of mathematical proof techniques to establish that a fragment of
a technical design possesses certain desirable (and formally stated)
properties.

Examples would be:

	is a specification consistent?
	does a particular loop always terminate?
	does a procedure always establish its post-condition?
	does a member-function always maintain its class invariant?
	does a logic design always satisfy its setup / hold time conditions?

Obviously, in the general case these problems are unsolvable. The ideas can
still be applied in practice, however, if you assume the philosophy that (eg)
a program is "guilty until proven innocent" - if you are unable to come up
with a proof that your program has the desired properties, then you modify it
until you can!

I am interested in verification applied to any design discipline, even though
research so far seems to have focussed on software (eg SPADE, MALPAS, Gypsy)
and digital logic (eg Viper). I am interested in everything from established
commercial products through to embryonic research projects, and IN PARTICULAR
I am interested in the mechanical TOOLS necessary to support these techniques
in practice and the mechanical THEOREM-PROVERS which are at the heart of these
tools. I am LESS (but still slightly) interested in the related techniques
of formal refinement (eg the B Method), whereby an implementation and its
proof are developed hand-in-hand.

Please e-mail me if you have any knowledge of any products, projects or similar
reviews which fall into this area. Many thanks.
-- 
Aaron Turner :-)

------- End of Forwarded Message