A manifesto for applicable formal methods

Mario Gleirscher*, Jaco van de Pol, Jim Woodcock

*Corresponding author for this work

Research output: Contribution to journalArticleAcademicpeer-review

2 Citations (Scopus)
7 Downloads (Pure)

Abstract

Recently, formal methods have been used in large industrial organisations (including AWS, Facebook/Meta, and Microsoft) and have proved to be an effective part of a software engineering process finding important bugs. Perhaps because of that, practitioners are interested in using them more often. Nevertheless, formal methods are far less applied than expected, particularly for safety-critical systems where they are strongly recommended and have the most significant potential. We hypothesise that formal methods still seem not applicable enough or ready for their intended use in such areas. 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 identify key challenges and lay out a set of guiding 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 increased use of formal methods in any appropriate context to the maximum benefit.

Original languageEnglish
Pages (from-to)1737-1749
Number of pages13
JournalSoftware and systems modeling
Volume22
Issue number6
Early online date18 Aug 2023
DOIs
Publication statusPublished - Dec 2023

Keywords

  • Formal methods
  • Formal verification
  • Research evaluation
  • Research transfer
  • Software engineering
  • Tools

Fingerprint

Dive into the research topics of 'A manifesto for applicable formal methods'. Together they form a unique fingerprint.

Cite this