Ralf Kneuper: Limits of Formal Methods
Formal Aspects of Computing, 9 (1997), S. 379-394.
When discussing the possibilities and limitations of formal methods, some people (often the `academics') take either a highly optimistic view, stressing possibilities and ignoring limitations, or (often developers from `the real world') a highly pessimistic view, describing certain limitations of formal methods and deducing that, since formal methods do not solve all our problems, they are useless. However, during the last few years, more people have started to promote a realistic view of the applicability of formal methods.
The main goal of this paper is to support this realistic view of the possibilities and limitations of formal methods (concentrating, as the title suggests, on their limitations, because the readership of this journal will already know all (well, almost) about their possibilities) To some extent, these limitations will seem quite obvious once stated, but in the author's experience, some parts of the formal methods community still do not fully realize them.
(pdf file, 199 kB)