A Manifesto for Applicable Formal Methods
Mario Gleirscher, Jaco van de Pol, Jim Woodcock

TL;DR
This paper advocates for a set of principles to enhance the applicability of formal methods in critical software engineering, aiming to bridge the gap between their proven effectiveness and limited practical adoption.
Contribution
It introduces a manifesto outlining principles for making formal methods more applicable and mature for practical use in critical domains.
Findings
Formal methods are effective but underused in critical domains.
A set of principles can guide the development of more applicable formal methods.
The manifesto aims to increase practical adoption of formal methods.
Abstract
Formal 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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsSoftware Engineering Research · Software Engineering Techniques and Practices · Model-Driven Software Engineering Techniques
