A Manifesto for Applicable Formal MethodsFormal methods were frequently shown to be effective and, perhaps because of
that, practitioners are interested in using them more often. Still, these
methods are far less applied than expected, particularly, in critical domains
where they are strongly recommended and where they have the greatest potential.
Our hypothesis is that formal methods still seem not to be applicable enough or
ready for their intended use. In critical software engineering, what do we mean
when we speak of a formal method? And what does it mean for such a method to be
applicable both from a scientific and practical viewpoint? Based on what the
literature tells about the first question, with this manifesto, we lay out a
set of principles that when followed by a formal method give rise to its mature
applicability in a given scope. Rather than exercising criticism of past
developments, this manifesto strives to foster an increased use of formal
methods to the maximum benefit.
arxiv.org